Repository navigation

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

Open

jrosain wants to merge 27 commits into

GoelandProver:masterfrom

jrosain:remove-indexes

Open

feat: remove invasive index in formulas and terms#71
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
- clean: remove useless indexes in formulas/terms
  jrosain
  committed
  33dcecd
- test-suite: remove indexes of bound variables in the .out
  jrosain
  committed
  202ec95
- upd: remove maker functions to keep only make functions
  jrosain
  committed
  e2fe52e
- clean: remove the useless method RenameVariables
  jrosain
  committed
  654b0f3

Commits

Commits on Aug 29, 2025

Commits on Feb 7, 2026

Commits on Feb 22, 2026

Commits on Mar 12, 2026

Commits on Apr 12, 2026