Module proof 

Read-only proof reconstruction API.

Structs

Proof

A proof shows that a Proposition is true, justified by a Justification.

ProofId

An identifier for a proof in a ProofStore

ProofStore

A ProofStore is similar to a TermDag. It’s a hash-consed arena enabling proofs to share sub-proofs. We refer to proofs with a ProofId which is an index into the store, used with ProofStore::get to retrieve the proof.

Proposition

In egglog, all proofs prove a Proposition, which is an equality between two terms. An egglog e-graph is a partial equality relation, closed under symmetry, transitivity, and congruence.

Enums

Justification

Justifies a Proposition using one of several proof rules. Some justifications are axioms of egglog, like Sym, Trans, and Congr. Other justifications are based on user input, like Fiat, Rule, and MergeFn.