def Lean.Meta.Grind.isInterpreted (e : Lean.Expr) : Lean.MetaM Bool

Returns true if e is True, False, or a literal value. See LitValues for supported literals.

Equations

• Lean.Meta.Grind.isInterpreted e = if (e.isTrue || e.isFalse) = true then pure true else do let y ← pure PUnit.unit (fun (y : PUnit) => Lean.Meta.isLitValue e) y

def Lean.Meta.Grind.mkENode (e : Lean.Expr) (generation : Nat := 0) : Lean.Meta.Grind.GoalM Unit

Creates an ENode for e if one does not already exist. This method assumes e has been hashconsed.

Equations

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

def Lean.Meta.Grind.getRoot (e : Lean.Expr) : Lean.Meta.Grind.GoalM Lean.Expr

Returns the root element in the equivalence class of e.

Equations

• Lean.Meta.Grind.getRoot e = do let __discr ← Lean.Meta.Grind.getENode? e match __discr with | some n => pure n.root | x => pure e

def Lean.Meta.Grind.getNext (e : Lean.Expr) : Lean.Meta.Grind.GoalM Lean.Expr

Returns the next element in the equivalence class of e.

Equations

• Lean.Meta.Grind.getNext e = do let __discr ← Lean.Meta.Grind.getENode? e match __discr with | some n => pure n.next | x => pure e

@[inline]

def Lean.Meta.Grind.isSameExpr (a b : Lean.Expr) : Bool

Equations

• Lean.Meta.Grind.isSameExpr a b = Lean.Meta.Grind.isSameExpr.unsafe_impl_1 a b

def Lean.Meta.Grind.addEqCore (lhs rhs proof : Lean.Expr) (isHEq : Bool) : Lean.Meta.Grind.GoalM Unit

Equations

• Lean.Meta.Grind.addEqCore lhs rhs proof isHEq = do Lean.Meta.Grind.addEqStep lhs rhs proof isHEq Lean.Meta.Grind.addEqCore.processTodo

partial def Lean.Meta.Grind.addEqCore.processTodo : Lean.Meta.Grind.GoalM Unit

def Lean.Meta.Grind.addEq (lhs rhs proof : Lean.Expr) : Lean.Meta.Grind.GoalM Unit

Equations

• Lean.Meta.Grind.addEq lhs rhs proof = Lean.Meta.Grind.addEqCore lhs rhs proof false

def Lean.Meta.Grind.addHEq (lhs rhs proof : Lean.Expr) : Lean.Meta.Grind.GoalM Unit

Equations

• Lean.Meta.Grind.addHEq lhs rhs proof = Lean.Meta.Grind.addEqCore lhs rhs proof true