structure Lean.Meta.Grind.Context : Type

• mainDeclName : Lean.Name

structure Lean.Meta.Grind.State : Type

• canon : Lean.Meta.Canonicalizer.State
• scState : ShareCommon.State Lean.ShareCommon.objectFactory

  ShareCommon (aka Hashconsing) state.

• nextThmIdx : Nat

  Next index for creating auxiliary theorems.

@[reducible, inline]

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

Equations

• Lean.Meta.Grind.GrindM = ReaderT Lean.Meta.Grind.Context (StateRefT' IO.RealWorld Lean.Meta.Grind.State Lean.MetaM)

@[inline]

def Lean.Meta.Grind.GrindM.run {α : Type} (x : Lean.Meta.Grind.GrindM α) (mainDeclName : Lean.Name) : Lean.MetaM α

Equations

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

def Lean.Meta.Grind.abstractNestedProofs (e : Lean.Expr) : Lean.Meta.Grind.GrindM Lean.Expr

Equations

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

def Lean.Meta.Grind.shareCommon (e : Lean.Expr) : Lean.Meta.Grind.GrindM Lean.Expr

Equations

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

def Lean.Meta.Grind.canon (e : Lean.Expr) : Lean.Meta.Grind.GrindM Lean.Expr

Equations

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

def Lean.Meta.Grind.canon.canonRec (e : Lean.Expr) : Lean.Meta.CanonM Lean.Expr

Equations

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

structure Lean.Meta.Grind.ENode : Type

Stores information for a node in the egraph. Each internalized expression e has an ENode associated with it.

• next : Lean.Expr

  Next element in the equivalence class.

• root : Lean.Expr

  Root (aka canonical representative) of the equivalence class

• cgRoot : Lean.Expr

  Root of the congruence class. This is field is a don't care if e is not an application.

• target? : Option Lean.Expr

  When e was added to this equivalence class because of an equality h : e = target, then we store target here, and h at proof?.

• proof? : Option Lean.Expr
• flipped : Bool

  Proof has been flipped.

• size : Nat

  Number of elements in the equivalence class, this field is meaningless if node is not the root.

• interpreted : Bool

  interpreted := true if node should be viewed as an abstract value.

• ctor : Bool

  ctor := true if the head symbol is a constructor application.

• hasLambdas : Bool

  hasLambdas := true if equivalence class contains lambda expressions.

• heqProofs : Bool

  If heqProofs := true, then some proofs in the equivalence class are based on heterogeneous equality.

• generation : Nat
• mt : Nat

  Modification time

structure Lean.Meta.Grind.Clause : Type

• expr : Lean.Expr
• proof : Lean.Expr

Instances For

• Lean.Meta.Grind.instInhabitedClause

instance Lean.Meta.Grind.instInhabitedClause : Inhabited Lean.Meta.Grind.Clause

Equations

• Lean.Meta.Grind.instInhabitedClause = { default := { expr := default, proof := default } }

def Lean.Meta.Grind.mkInputClause (fvarId : Lean.FVarId) : Lean.MetaM Lean.Meta.Grind.Clause

Equations

• Lean.Meta.Grind.mkInputClause fvarId = do let __do_lift ← fvarId.getType pure { expr := __do_lift, proof := Lean.mkFVar fvarId }

structure Lean.Meta.Grind.NewEq : Type

• lhs : Lean.Expr
• rhs : Lean.Expr
• proof : Lean.Expr
• isHEq : Bool

structure Lean.Meta.Grind.Goal : Type

• mvarId : Lean.MVarId
• clauses : Lean.PArray Lean.Meta.Grind.Clause
• enodes : Lean.PHashMap USize Lean.Meta.Grind.ENode
• newEqs : Array Lean.Meta.Grind.NewEq
• inconsistent : Bool

  inconsistent := true if ENodes for True and False are in the same equivalence class.

• gmt : Nat

  Goal modification time.

Instances For

• Lean.Meta.Grind.instInhabitedGoal

instance Lean.Meta.Grind.instInhabitedGoal : Inhabited Lean.Meta.Grind.Goal

Equations

• Lean.Meta.Grind.instInhabitedGoal = { default := { mvarId := default, clauses := default, enodes := default, newEqs := default, inconsistent := default, gmt := default } }

def Lean.Meta.Grind.Goal.admit (goal : Lean.Meta.Grind.Goal) : Lean.MetaM Unit

Equations

• goal.admit = goal.mvarId.admit

@[reducible, inline]

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

Equations

• Lean.Meta.Grind.GoalM = StateRefT' IO.RealWorld Lean.Meta.Grind.Goal Lean.Meta.Grind.GrindM

@[inline]

def Lean.Meta.Grind.GoalM.run {α : Type} (goal : Lean.Meta.Grind.Goal) (x : Lean.Meta.Grind.GoalM α) : Lean.Meta.Grind.GrindM (α × Lean.Meta.Grind.Goal)

Equations

• Lean.Meta.Grind.GoalM.run goal x = StateRefT'.run x goal

@[inline]

def Lean.Meta.Grind.GoalM.run' (goal : Lean.Meta.Grind.Goal) (x : Lean.Meta.Grind.GoalM Unit) : Lean.Meta.Grind.GrindM Lean.Meta.Grind.Goal

Equations

• Lean.Meta.Grind.GoalM.run' goal x = (x *> get).run' goal

def Lean.Meta.Grind.getENode? (e : Lean.Expr) : Lean.Meta.Grind.GoalM (Option Lean.Meta.Grind.ENode)

Returns some n if e has already been "internalized" into the Otherwise, returns nones.

Equations

• Lean.Meta.Grind.getENode? e = do let __do_lift ← get pure (Lean.PersistentHashMap.find? __do_lift.enodes (Lean.Meta.Grind.getENode?.unsafe_impl_1 e))

def Lean.Meta.Grind.setENode (e : Lean.Expr) (n : Lean.Meta.Grind.ENode) : Lean.Meta.Grind.GoalM Unit

Equations

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

def Lean.Meta.Grind.mkENodeCore (e : Lean.Expr) (interpreted ctor : Bool) (generation : Nat) : Lean.Meta.Grind.GoalM Unit

Equations

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

def Lean.Meta.Grind.mkGoal (mvarId : Lean.MVarId) : Lean.Meta.Grind.GrindM Lean.Meta.Grind.Goal

Equations

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