structure Lean.Meta.Grind.AC.ProofM.State : Type

• cache : Std.HashMap UInt64 Expr
• varDecls : Std.HashMap Grind.AC.Var Expr
• exprDecls : Std.HashMap Grind.AC.Expr Expr
• seqDecls : Std.HashMap Grind.AC.Seq Expr

structure Lean.Meta.Grind.AC.ProofM.Context : Type

• ctx : Expr

@[reducible, inline]

abbrev Lean.Meta.Grind.AC.ProofM (α : Type) : Type

Equations

• Lean.Meta.Grind.AC.ProofM = ReaderT Lean.Meta.Grind.AC.ProofM.Context (StateRefT' IO.RealWorld Lean.Meta.Grind.AC.ProofM.State Lean.Meta.Grind.AC.ACM)

partial def Lean.Meta.Grind.AC.EqCnstr.toExprProof (c : EqCnstr) : ProofM Expr

partial def Lean.Meta.Grind.AC.DiseqCnstr.toExprProof (c : DiseqCnstr) : ProofM Expr

def Lean.Meta.Grind.AC.DiseqCnstr.setUnsat (c : DiseqCnstr) : ACM Unit

Equations

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

def Lean.Meta.Grind.AC.mkExprEqSeqProof (e : Grind.AC.Expr) (c : EqCnstr) : ProofM Expr

Equations

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

def Lean.Meta.Grind.AC.propagateEq (a b : Expr) (ea eb : Grind.AC.Expr) (ca cb : EqCnstr) : ACM Unit

Asserts a = b, where

• ea is as reification
• eb is bs reification
• ca is a proof for sa = s where norm ea = sa
• cb is a proof for sb = s where norm eb = sb

Equations

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