A basic "equality resolution" procedure.

structure Lean.Meta.Grind.TopSort.State : Type

• tempMark : Std.HashSet Expr
• permMark : Std.HashSet Expr
• result : Array Expr

@[reducible, inline]

abbrev Lean.Meta.Grind.TopSortM (α : Type) : Type

Equations

• Lean.Meta.Grind.TopSortM = OptionT (StateT Lean.Meta.Grind.TopSort.State Lean.MetaM)

def Lean.Meta.Grind.eqResolution (prop : Expr) : MetaM (Option (Expr × Expr))

A basic "equality resolution" procedure: Given a proposition prop with a proof proof, it attempts to resolve equality hypotheses using isDefEq. For example, it reduces ∀ x y, f x = f (g y y) → g x y = y to ∀ y, g (g y y) y = y, and ∀ (x : Nat), f x ≠ f a to False. If successful, the result is a pair (prop', proof), where prop' is the simplified proposition, and proof : prop → prop'

Equations

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