Facts collection for the order Tactic

This file implements the collection of facts for the order tactic.

inductive Mathlib.Tactic.Order.AtomicFact : Type

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

instance Mathlib.Tactic.Order.instInhabitedAtomicFact : Inhabited AtomicFact

Equations

• Mathlib.Tactic.Order.instInhabitedAtomicFact = { default := Mathlib.Tactic.Order.AtomicFact.eq default default default }

instance Mathlib.Tactic.Order.instBEqAtomicFact : BEq AtomicFact

Equations

• Mathlib.Tactic.Order.instBEqAtomicFact = { beq := Mathlib.Tactic.Order.beqAtomicFact✝ }

instance Mathlib.Tactic.Order.instToStringAtomicFact : ToString AtomicFact

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Mathlib.Tactic.Order.CollectFactsState : Type

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 AtomicFacts about them.

Equations

• Mathlib.Tactic.Order.CollectFactsState = Std.HashMap Lean.Expr (Lean.Meta.DiscrTree (ℕ × Lean.Expr) × Array Mathlib.Tactic.Order.AtomicFact)

@[reducible, inline]

abbrev Mathlib.Tactic.Order.CollectFactsM (α : Type) : Type

Monad for the fact collection procedure.

Equations

• Mathlib.Tactic.Order.CollectFactsM = StateT Mathlib.Tactic.Order.CollectFactsState Lean.MetaM

def Mathlib.Tactic.Order.addAtom {u : Lean.Level} (type : Q(Type u)) (x : Q(«$type»)) : CollectFactsM ℕ

Updates the state with the atom x.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Order.addFact (type : Lean.Expr) (fact : AtomicFact) : CollectFactsM Unit

Adds fact to the state.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Order.collectFactsImp (g : Lean.MVarId) : CollectFactsM Unit

Implementation for collectFacts in CollectFactsM monad.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Order.collectFactsImp.processExpr (expr : Lean.Expr) : CollectFactsM Unit

Extracts facts and atoms from the expression.

def Mathlib.Tactic.Order.collectFacts (g : Lean.MVarId) : Lean.MetaM (Std.HashMap Lean.Expr (Std.HashMap ℕ Lean.Expr × Array AtomicFact))

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 AtomicFacts about them.

Equations

• One or more equations did not get rendered due to their size.