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

def Lean.Meta.Grind.add (fact proof : Lean.Expr) (generation : Nat := 0) : Lean.Meta.Grind.GoalM Unit

Adds a new fact justified by the given proof and using the given generation.

Equations

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

def Lean.Meta.Grind.add.go (proof : Lean.Expr) (generation : Nat := 0) (p : Lean.Expr) (isNeg : Bool) : Lean.Meta.Grind.GoalM Unit

Equations

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

def Lean.Meta.Grind.add.goEq (proof : Lean.Expr) (generation : Nat := 0) (p lhs rhs : Lean.Expr) (isNeg isHEq : Bool) : Lean.Meta.Grind.GoalM Unit

Equations

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

def Lean.Meta.Grind.addHypothesis (fvarId : Lean.FVarId) (generation : Nat := 0) : Lean.Meta.Grind.GoalM Unit

Adds a new hypothesis.

Equations

• Lean.Meta.Grind.addHypothesis fvarId generation = do let __do_lift ← liftM fvarId.getType Lean.Meta.Grind.add __do_lift (Lean.mkFVar fvarId) generation