Documentation

Lean.Meta.Tactic.Grind.Arith.Insts

source
def Lean.Meta.Grind.Arith.getIsCharInst? (u : Level) (type semiringInst : Expr) :
GoalM (Option (Expr × Nat))
Equations
    Instances For
      source
      def Lean.Meta.Grind.Arith.getNoZeroDivInst? (u : Level) (type : Expr) :
      GoalM (Option Expr)
      Equations
        Instances For