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

• Lean.Meta.DefEq.isInstNegInt e = do let __do_lift ← Lean.Meta.Structural.isInstNegInt e if __do_lift = true then pure true else Lean.Meta.isDefEqI e Lean.Int.mkInstNeg

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

Equations

• Lean.Meta.DefEq.isInstAddInt e = do let __do_lift ← Lean.Meta.Structural.isInstAddInt e if __do_lift = true then pure true else Lean.Meta.isDefEqI e Lean.Int.mkInstAdd

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

Equations

• Lean.Meta.DefEq.isInstHAddInt e = do let __do_lift ← Lean.Meta.Structural.isInstHAddInt e if __do_lift = true then pure true else Lean.Meta.isDefEqI e Lean.Int.mkInstHAdd

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

Equations

• Lean.Meta.DefEq.isInstSubInt e = do let __do_lift ← Lean.Meta.Structural.isInstSubInt e if __do_lift = true then pure true else Lean.Meta.isDefEqI e Lean.Int.mkInstSub

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

Equations

• Lean.Meta.DefEq.isInstHSubInt e = do let __do_lift ← Lean.Meta.Structural.isInstHSubInt e if __do_lift = true then pure true else Lean.Meta.isDefEqI e Lean.Int.mkInstHSub

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

Equations

• Lean.Meta.DefEq.isInstMulInt e = do let __do_lift ← Lean.Meta.Structural.isInstMulInt e if __do_lift = true then pure true else Lean.Meta.isDefEqI e Lean.Int.mkInstMul

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

Equations

• Lean.Meta.DefEq.isInstHMulInt e = do let __do_lift ← Lean.Meta.Structural.isInstHMulInt e if __do_lift = true then pure true else Lean.Meta.isDefEqI e Lean.Int.mkInstHMul

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

Equations

• Lean.Meta.DefEq.isInstLTInt e = do let __do_lift ← Lean.Meta.Structural.isInstLTInt e if __do_lift = true then pure true else Lean.Meta.isDefEqI e Lean.Int.mkInstLT

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

Equations

• Lean.Meta.DefEq.isInstLEInt e = do let __do_lift ← Lean.Meta.Structural.isInstLEInt e if __do_lift = true then pure true else Lean.Meta.isDefEqI e Lean.Int.mkInstLE

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

Equations

• Lean.Meta.DefEq.isInstDvdInt e = do let __do_lift ← Lean.Meta.Structural.isInstDvdInt e if __do_lift = true then pure true else Lean.Meta.isDefEqI e (Lean.mkConst `Int.instDvd)