source
def Lean.Meta.Grind.addCongrTable (e : Expr) :
GoalM Unit

Adds `e` to congruence table.

Equations

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

Instances For

source
def Lean.Meta.Grind.isMorallyIff (e : Expr) :
Bool

Returns `true` if `e` is of the form `@Eq Prop a b`

Equations

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

Instances For

source
def Lean.Meta.Grind.activateTheorem (thm : EMatchTheorem) (generation : Nat) :
GoalM Unit
Equations

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

Instances For