Functions for testing whether expressions are canonical Int instances.

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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