def Lean.Meta.Grind.Arith.isNatType (e : Expr) : Bool

Returns true if e is of the form Nat

Equations

• Lean.Meta.Grind.Arith.isNatType e = e.isConstOf `Nat

def Lean.Meta.Grind.Arith.isInstAddNat (e : Expr) : Bool

Returns true if e is of the form @instHAdd Nat instAddNat

Equations

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

def Lean.Meta.Grind.Arith.isInstLENat (e : Expr) : Bool

Returns true if e is instLENat

Equations

• Lean.Meta.Grind.Arith.isInstLENat e = e.isConstOf `instLENat

def Lean.Meta.Grind.Arith.isNatAdd? (e : Expr) : Option (Expr × Expr)

Returns some (a, b) if e is of the form

@HAdd.hAdd Nat Nat Nat (instHAdd Nat instAddNat) a b

Equations

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

def Lean.Meta.Grind.Arith.isNatAdd (e : Expr) : Bool

Returns true if e is of the form

@HAdd.hAdd Nat Nat Nat (instHAdd Nat instAddNat) _ _

Equations

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

def Lean.Meta.Grind.Arith.isNatNum? (e : Expr) : Option Nat

Returns some k if e @OfNat.ofNat Nat _ (instOfNatNat k)

Equations

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