Lean.Meta.IntInstTesters

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.

source

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

MetaM Bool

Equations

Instances For

source

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

MetaM Bool

Equations

Instances For

source

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

MetaM Bool

Equations

Instances For

source

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

MetaM Bool

Equations

Instances For

source

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

MetaM Bool

Equations

Instances For

source

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

MetaM Bool

Equations

Instances For

source

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

MetaM Bool

Equations

Instances For

source

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

MetaM Bool

Equations

Instances For

source

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

MetaM Bool

Equations

Instances For

source

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

MetaM Bool

Equations

Instances For

source

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

MetaM Bool

Equations

Instances For

source

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

MetaM Bool

Equations

Instances For

source

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

MetaM Bool

Equations

Instances For

source

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

MetaM Bool

Equations

Instances For

source

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

MetaM Bool

Equations

Instances For

source

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

MetaM Bool

Equations

Instances For

source

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

MetaM Bool

Equations

Instances For

source

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

MetaM Bool

Equations

Instances For

source

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

MetaM Bool

Equations

Instances For

source

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

MetaM Bool

Equations

Instances For

source

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

MetaM Bool

Equations

Instances For

source

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

MetaM Bool

Equations

Instances For

source

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

MetaM Bool

Equations

Instances For

source

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

MetaM Bool

Equations

Instances For

source

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

MetaM Bool

Equations

Instances For

source

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

MetaM Bool

Equations

Instances For

source

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

MetaM Bool

Equations

Instances For

source

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

MetaM Bool

Equations

Instances For