Expand description
A proof format for egglog programs, based on the Rocq format and checker from Tia Vu, Ryan Doegens, and Oliver Flatt.
Structs§
- Cong
Proof - EqProof
Id - an id identifying proofs of equality between two terms within a
ProofStore - Pretty
Print Config - Proof
Store - A hash-cons store for proofs and terms related to an egglog program.
- TermDag
- TermId
- an id identifying terms within a
TermDag - Term
Proof Id - an id identifying proofs of terms within a
ProofStore