Facts collection for the order
Tactic #
This file implements the collection of facts for the order
tactic.
A structure for storing facts about variables.
- eq (lhs rhs : ℕ) (proof : Lean.Expr) : AtomicFact
- ne (lhs rhs : ℕ) (proof : Lean.Expr) : AtomicFact
- le (lhs rhs : ℕ) (proof : Lean.Expr) : AtomicFact
- nle (lhs rhs : ℕ) (proof : Lean.Expr) : AtomicFact
- lt (lhs rhs : ℕ) (proof : Lean.Expr) : AtomicFact
- nlt (lhs rhs : ℕ) (proof : Lean.Expr) : AtomicFact
Instances For
@[reducible, inline]
State for CollectFactsM
. It contains a map where the key t
maps to a
pair (atomToIdx, facts)
. atomToIdx
is a DiscrTree
containing atomic expressions with their
indices, and facts
stores AtomicFact
s about them.
Equations
Instances For
@[reducible, inline]
Monad for the fact collection procedure.
Equations
Instances For
Updates the state with the atom x
.
Equations
Instances For
Adds fact
to the state.
Equations
Instances For
Extracts facts and atoms from the expression.
Equations
Instances For
Collects facts from the local context. For each occurring type α
, the returned map contains
a pair (idxToAtom, facts)
, where the map idxToAtom
converts indices to found
atomic expressions of type α
, and facts
contains all collected AtomicFact
s about them.