Functions for testing whether expressions are canonical Int instances.

Note: Structural tests are syntactic. They are more efficient, but should be used only in modules that have perform some kind of canonicalization.

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Meta.Structural.isInstNatPowInt (e : Expr) : MetaM Bool

Equations

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

def Lean.Meta.Structural.isInstPowInt (e : Expr) : MetaM Bool

Equations

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

def Lean.Meta.Structural.isInstHPowInt (e : Expr) : MetaM Bool

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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