Documentation

Lean.Meta.NatInstTesters

Functions for testing whether expressions are canonical Nat instances.

source
def Lean.Meta.isInstOfNatNat (e : Expr) :
MetaM Bool
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.isInstAddNat (e : Expr) :
MetaM Bool
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.isInstSubNat (e : Expr) :
MetaM Bool
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.isInstMulNat (e : Expr) :
MetaM Bool
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.isInstDivNat (e : Expr) :
MetaM Bool
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.isInstModNat (e : Expr) :
MetaM Bool
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.isInstNatPowNat (e : Expr) :
MetaM Bool
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.isInstPowNat (e : Expr) :
MetaM Bool
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.isInstHAddNat (e : Expr) :
MetaM Bool
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.isInstHSubNat (e : Expr) :
MetaM Bool
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.isInstHMulNat (e : Expr) :
MetaM Bool
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.isInstHDivNat (e : Expr) :
MetaM Bool
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.isInstHModNat (e : Expr) :
MetaM Bool
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.isInstHPowNat (e : Expr) :
MetaM Bool
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.isInstLTNat (e : Expr) :
MetaM Bool
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.isInstLENat (e : Expr) :
MetaM Bool
Equations
  • One or more equations did not get rendered due to their size.