Add `IProof` interface with a tree structure and add relevant adapter for `[]Search.ProofStruct` - #64

Open

jrosain wants to merge 20 commits into

GoelandProver:masterfrom

jrosain:add-proof-adapter

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

Navigation Menu

Uh oh!

Add `IProof` interface with a tree structure and add relevant adapter for `[]Search.ProofStruct` - #64

Add `IProof` interface with a tree structure and add relevant adapter for `[]Search.ProofStruct`#64
jrosain wants to merge 20 commits into
GoelandProver:masterfrom
jrosain:add-proof-adapter

Commits on Aug 29, 2025

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

Commits on Feb 7, 2026

Upd: coq -> rocq in the output

Fix: avoid keeping formulas in GS3 sequent structure to use less memory

Removal of invasive type system

Updated syntax of types and reintroduced them in the internals

Implementation of the new typing system

Updated gamma and delta rules to deal with type variables

Manage typed proof search and add related tests

Fix equality of quantified formulas (forall, exists)

Add proper debugging facilities in typing rules

Add some basic tests on the elaboration

Replace MappableString with a proper printing management

Define printer for Rocq output

Add systematic rocq compilation when running test suite

Add rocq installation in GitHub test-suite workflow

Add: proof-certification folder with instructions on how to certify proofs with Goeland

Add: use lambdapi to check the test-suite

Fix: use new printer system to have a valid lambdapi output

Upd: update contributing to include test-suite instructions (and special instructions for lambdapi)

Add proof interface and adapter for Search.ProofStruct