SimonGuilloud
commented
11 months ago - Add ids to terms like for formulas
- Add serialization of proofs. Theorems can be serialized to binary files and loaded back on later run.
- On my machine, running everything up to Recursion.scala takes 19s instead of 24s.
- Does no hash consing, but simple optimizations to proof size (remove consecutive rewrites, flatten subproofs)
- Cleans up the distinction between fullName (with the whole path, should be unique) and name (just the last part, possibly duplicate across different files/domains).
- Good completion of documentation in WithTheorems
- checkProofs does not print proofs of more thant 100 steps now.
- fixed an indexing bug in ShrinkProof.flattenProof
- Suite of tests for serialization, export then load a collection of theorems.
- Push suite of tests for Tableaux tactic that were missing.
Tool to export proofs of theorems to binary files and back.