def Lean.Meta.Grind.AC.instHashableSeq_lean.hash : Grind.AC.Seq → UInt64

@[implicit_reducible]

instance Lean.Meta.Grind.AC.instHashableSeq_lean : Hashable Grind.AC.Seq

@[implicit_reducible]

instance Lean.Meta.Grind.AC.instHashableExpr_lean : Hashable Grind.AC.Expr

def Lean.Meta.Grind.AC.instHashableExpr_lean.hash : Grind.AC.Expr → UInt64

structure Lean.Meta.Grind.AC.EqCnstr : Type

• lhs : Grind.AC.Seq
• rhs : Grind.AC.Seq
• h : EqCnstrProof
• id : Nat

inductive Lean.Meta.Grind.AC.EqCnstrProof : Type

• core (a b : Expr) (ea eb : Grind.AC.Expr) : EqCnstrProof
• erase_dup (c : EqCnstr) : EqCnstrProof
• erase0 (c : EqCnstr) : EqCnstrProof
• swap (c : EqCnstr) : EqCnstrProof
• simp_exact (lhs : Bool) (c₁ c₂ : EqCnstr) : EqCnstrProof
• simp_ac (lhs : Bool) (s : Grind.AC.Seq) (c₁ c₂ : EqCnstr) : EqCnstrProof
• simp_suffix (lhs : Bool) (s : Grind.AC.Seq) (c₁ c₂ : EqCnstr) : EqCnstrProof
• simp_prefix (lhs : Bool) (s : Grind.AC.Seq) (c₁ c₂ : EqCnstr) : EqCnstrProof
• simp_middle (lhs : Bool) (s₁ s₂ : Grind.AC.Seq) (c₁ c₂ : EqCnstr) : EqCnstrProof
• superpose_ac (r₁ c r₂ : Grind.AC.Seq) (c₁ c₂ : EqCnstr) : EqCnstrProof
• superpose (p s c : Grind.AC.Seq) (c₁ c₂ : EqCnstr) : EqCnstrProof
• superpose_ac_idempotent (x : Grind.AC.Var) (c₁ : EqCnstr) : EqCnstrProof
• superpose_head_idempotent (x : Grind.AC.Var) (c₁ : EqCnstr) : EqCnstrProof
• superpose_tail_idempotent (x : Grind.AC.Var) (c₁ : EqCnstr) : EqCnstrProof
• refl (s : Grind.AC.Seq) : EqCnstrProof
• erase_dup_rhs (c : EqCnstr) : EqCnstrProof
• erase0_rhs (c : EqCnstr) : EqCnstrProof

@[implicit_reducible]

instance Lean.Meta.Grind.AC.instInhabitedEqCnstrProof : Inhabited EqCnstrProof

@[implicit_reducible]

instance Lean.Meta.Grind.AC.instInhabitedEqCnstr : Inhabited EqCnstr

def Lean.Meta.Grind.AC.EqCnstr.compare (c₁ c₂ : EqCnstr) : Ordering

@[reducible, inline]

abbrev Lean.Meta.Grind.AC.Queue : Type

structure Lean.Meta.Grind.AC.DiseqCnstr : Type

• lhs : Grind.AC.Seq
• rhs : Grind.AC.Seq
• h : DiseqCnstrProof

inductive Lean.Meta.Grind.AC.DiseqCnstrProof : Type

• core (a b : Expr) (ea eb : Grind.AC.Expr) : DiseqCnstrProof
• erase_dup (c : DiseqCnstr) : DiseqCnstrProof
• erase0 (c : DiseqCnstr) : DiseqCnstrProof
• simp_exact (lhs : Bool) (c₁ : EqCnstr) (c₂ : DiseqCnstr) : DiseqCnstrProof
• simp_ac (lhs : Bool) (s : Grind.AC.Seq) (c₁ : EqCnstr) (c₂ : DiseqCnstr) : DiseqCnstrProof
• simp_suffix (lhs : Bool) (s : Grind.AC.Seq) (c₁ : EqCnstr) (c₂ : DiseqCnstr) : DiseqCnstrProof
• simp_prefix (lhs : Bool) (s : Grind.AC.Seq) (c₁ : EqCnstr) (c₂ : DiseqCnstr) : DiseqCnstrProof
• simp_middle (lhs : Bool) (s₁ s₂ : Grind.AC.Seq) (c₁ : EqCnstr) (c₂ : DiseqCnstr) : DiseqCnstrProof

structure Lean.Meta.Grind.AC.Struct : Type

• id : Nat
• type : Expr
• u : Level

  Cached getLevel type

• op : Expr
• neutral? : Option Expr
• assocInst : Expr
• idempotentInst? : Option Expr
• commInst? : Option Expr
• neutralInst? : Option Expr
• nextId : Nat

  Next unique id for EqCnstrs.

• vars : PArray Expr

  Mapping from variables to their denotations. Remark each variable can be in only one ring.

• varMap : PHashMap ExprPtr Grind.AC.Var

  Mapping from Expr to a variable representing it.

• denote : PHashMap ExprPtr Grind.AC.Expr

  Mapping from Lean expressions to their representations as AC.Expr

• denoteEntries : PArray (Expr × Grind.AC.Expr)

  denoteEntries is denote as a PArray for deterministic traversal.

• queue : Queue

  Equations to process.

• basis : List EqCnstr

  Processed equations.

• diseqs : PArray DiseqCnstr

  Disequalities.

• recheck : Bool

  If recheck is true, then new equalities have been added to the basis since we checked disequalities and implied equalities.

def Lean.Meta.Grind.AC.instInhabitedStruct.default : Struct

@[implicit_reducible]

instance Lean.Meta.Grind.AC.instInhabitedStruct : Inhabited Struct

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

State for all associative operators detected by grind.

• structs : Array Struct

  Structures/operators detected. We expect to find a small number of associative operators in a given goal. Thus, using Array is fine here.

• opIdOf : PHashMap ExprPtr (Option Nat)

  Mapping from operators to its "operator id". We cache failures using none. opIdOf[op] is some id, then id < structs.size.

• exprToOpIds : PHashMap ExprPtr (List Nat)

  Mapping from expressions/terms to their structure ids. Recall that term may be the argument of different operators.

• steps : Nat

def Lean.Meta.Grind.AC.instInhabitedState.default : State

@[implicit_reducible]

instance Lean.Meta.Grind.AC.instInhabitedState : Inhabited State

opaque Lean.Meta.Grind.AC.acExt : SolverExtension State