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

Equations

• Lean.Meta.Grind.AC.instHashableSeq_lean.hash (Lean.Grind.AC.Seq.var a) = mixHash 0 (hash a)
• Lean.Meta.Grind.AC.instHashableSeq_lean.hash (Lean.Grind.AC.Seq.cons a a_1) = mixHash (mixHash 1 (hash a)) (Lean.Meta.Grind.AC.instHashableSeq_lean.hash a_1)

@[implicit_reducible]

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

Equations

• Lean.Meta.Grind.AC.instHashableSeq_lean = { hash := Lean.Meta.Grind.AC.instHashableSeq_lean.hash }

@[implicit_reducible]

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

Equations

• Lean.Meta.Grind.AC.instHashableExpr_lean = { hash := Lean.Meta.Grind.AC.instHashableExpr_lean.hash }

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

Equations

• Lean.Meta.Grind.AC.instHashableExpr_lean.hash (Lean.Grind.AC.Expr.var a) = mixHash 0 (hash a)
• Lean.Meta.Grind.AC.instHashableExpr_lean.hash (a.op a_1) = mixHash (mixHash 1 (Lean.Meta.Grind.AC.instHashableExpr_lean.hash a)) (Lean.Meta.Grind.AC.instHashableExpr_lean.hash a_1)

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

Equations

• Lean.Meta.Grind.AC.instInhabitedEqCnstrProof = { default := Lean.Meta.Grind.AC.EqCnstrProof.core default default default default }

@[implicit_reducible]

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

Equations

• Lean.Meta.Grind.AC.instInhabitedEqCnstr = { default := { lhs := default, rhs := default, h := default, id := 0 } }

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

Equations

• c₁.compare c₂ = (compare c₁.lhs.length c₂.lhs.length).then (compare c₁.id c₂.id)

@[reducible, inline]

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

Equations

• Lean.Meta.Grind.AC.Queue = Std.TreeSet Lean.Meta.Grind.AC.EqCnstr Lean.Meta.Grind.AC.EqCnstr.compare

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.

@[implicit_reducible]

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

Equations

• Lean.Meta.Grind.AC.instInhabitedStruct = { default := Lean.Meta.Grind.AC.instInhabitedStruct.default }

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

@[implicit_reducible]

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

Equations

• Lean.Meta.Grind.AC.instInhabitedState = { default := Lean.Meta.Grind.AC.instInhabitedState.default }

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