feat: remove invasive index in formulas and terms - #71

Open

jrosain wants to merge 27 commits into

GoelandProver:masterfrom

jrosain:remove-indexes

Commits on Aug 29, 2025

Clean: replace *FormList by Lib.List[Form]
jrosain
committed
b33e6ae

Commits on Feb 7, 2026

Upd: coq -> rocq in the output
jrosain
committed
4bad89b
Fix: avoid keeping formulas in GS3 sequent structure to use less memory
jrosain
committed
037d198
Removal of invasive type system
jrosain
committed
09303f7
Updated syntax of types and reintroduced them in the internals
jrosain
committed
6c5dbac
Implementation of the new typing system
jrosain
committed
75610ed
Updated gamma and delta rules to deal with type variables
jrosain
committed
1e53850
Manage typed proof search and add related tests
jrosain
committed
403fef0
Fix equality of quantified formulas (forall, exists)
jrosain
committed
b82aee9
Add proper debugging facilities in typing rules
jrosain
committed
205c7fe
Add some basic tests on the elaboration
jrosain
committed
0c627a3
Replace MappableString with a proper printing management
jrosain
committed
59cb149
Define printer for Rocq output
jrosain
committed
e534bf1
Add systematic rocq compilation when running test suite
jrosain
committed
1b5a8e8
Add rocq installation in GitHub test-suite workflow
jrosain
committed
6d8ef73
Add: proof-certification folder with instructions on how to certify proofs with Goeland
jrosain
committed
8446313
Add: use lambdapi to check the test-suite
jrosain
committed
f5f429b
Fix: use new printer system to have a valid lambdapi output
jrosain
committed
720be91
Upd: update contributing to include test-suite instructions (and special instructions for lambdapi)
jrosain
committed
dacea15
Add proof interface and adapter for Search.ProofStruct
jrosain
committed
85f405e

Commits on Feb 22, 2026

Add: golines as a dependency to avoid having lines over a 100 characters
jrosain
committed
99329c8

Commits on Mar 12, 2026

fix: Rework deskolemization algorithm and adapt proof outputs to IProof
jrosain
committed
104d20d
add: update test-suite
jrosain
committed
e2d8d75

Commits on Apr 12, 2026