Functions for testing whether expressions are canonical Nat instances.

def Lean.Meta.isInstOfNatNat (e : Expr) : MetaM Bool

Equations

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

def Lean.Meta.isInstAddNat (e : Expr) : MetaM Bool

Equations

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

def Lean.Meta.isInstSubNat (e : Expr) : MetaM Bool

Equations

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

def Lean.Meta.isInstMulNat (e : Expr) : MetaM Bool

Equations

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

def Lean.Meta.isInstDivNat (e : Expr) : MetaM Bool

Equations

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

def Lean.Meta.isInstModNat (e : Expr) : MetaM Bool

Equations

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

def Lean.Meta.isInstNatPowNat (e : Expr) : MetaM Bool

Equations

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

def Lean.Meta.isInstPowNat (e : Expr) : MetaM Bool

Equations

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

def Lean.Meta.isInstHAddNat (e : Expr) : MetaM Bool

Equations

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

def Lean.Meta.isInstHSubNat (e : Expr) : MetaM Bool

Equations

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

def Lean.Meta.isInstHMulNat (e : Expr) : MetaM Bool

Equations

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

def Lean.Meta.isInstHDivNat (e : Expr) : MetaM Bool

Equations

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

def Lean.Meta.isInstHModNat (e : Expr) : MetaM Bool

Equations

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

def Lean.Meta.isInstHPowNat (e : Expr) : MetaM Bool

Equations

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

def Lean.Meta.isInstLTNat (e : Expr) : MetaM Bool

Equations

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

def Lean.Meta.isInstLENat (e : Expr) : MetaM Bool

Equations

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

def Lean.Meta.isInstDvdNat (e : Expr) : MetaM Bool

Equations

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