Repository navigation

feat: De-Bruijn Style Nameless Bound Variables - #79

Open

jrosain wants to merge 30 commits into

GoelandProver:masterfrom

jrosain:anonymous-de-bruijn

Open

feat: De-Bruijn Style Nameless Bound Variables#79
jrosain wants to merge 30 commits into
GoelandProver:masterfrom
jrosain:anonymous-de-bruijn

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 Mar 20, 2026
- clean: remove useless indexes in formulas/terms
  jrosain
  committed
  2b65427
- test-suite: remove indexes of bound variables in the .out
  jrosain
  committed
  6274fc0
- upd: remove maker functions to keep only make functions
  jrosain
  committed
  5b59b35
- clean: remove the useless method RenameVariables
  jrosain
  committed
  d28bf89
Commits on Mar 26, 2026
- clean: remove TermForm and unify terms
  jrosain
  committed
  b23a76b
- clean: nameless bound variables
  jrosain
  committed
  ed4d701
- upd: test-suite output update with nameless variables
  jrosain
  committed
  591af82

Commits

Commits on Aug 29, 2025

Commits on Feb 7, 2026

Commits on Feb 22, 2026

Commits on Mar 12, 2026

Commits on Mar 20, 2026

Commits on Mar 26, 2026