Documentation

Lean.Meta.Tactic.Grind.Arith.Insts

source
def Lean.Meta.Grind.Arith.getIsCharInst? (u : Level) (type semiringInst : Expr) :
GoalM (Option (Expr × Nat))
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.Meta.Grind.Arith.getNoZeroDivInst? (u : Level) (type : Expr) :
    GoalM (Option Expr)
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For