def Lean.Meta.Grind.Arith.isNatType (e : Expr) : Bool

Returns true if e is of the form Nat

Equations

• Lean.Meta.Grind.Arith.isNatType e = e.isConstOf `Nat

def Lean.Meta.Grind.Arith.isInstAddNat (e : Expr) : Bool

Returns true if e is of the form @instHAdd Nat instAddNat

Equations

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

def Lean.Meta.Grind.Arith.isInstLENat (e : Expr) : Bool

Returns true if e is instLENat

Equations

• Lean.Meta.Grind.Arith.isInstLENat e = e.isConstOf `instLENat

def Lean.Meta.Grind.Arith.isNatAdd? (e : Expr) : Option (Expr × Expr)

Returns some (a, b) if e is of the form

@HAdd.hAdd Nat Nat Nat (instHAdd Nat instAddNat) a b

Equations

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

def Lean.Meta.Grind.Arith.isNatAdd (e : Expr) : Bool

Returns true if e is of the form

@HAdd.hAdd Nat Nat Nat (instHAdd Nat instAddNat) _ _

Equations

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

def Lean.Meta.Grind.Arith.isNatNum? (e : Expr) : Option Nat

Returns some k if e @OfNat.ofNat Nat _ (instOfNatNat k)

Equations

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

def Lean.Meta.Grind.Arith.isNatOffset? (e : Expr) : Option (Expr × Nat)

Returns some (a, k) if e is of the form a + k.

Equations

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

structure Lean.Meta.Grind.Arith.Offset.Cnstr (α : Type) : Type

An offset constraint.

• u : α
• v : α
• k : Int

instance Lean.Meta.Grind.Arith.Offset.instInhabitedCnstr {a✝ : Type} [Inhabited a✝] : Inhabited (Cnstr a✝)

Equations

• Lean.Meta.Grind.Arith.Offset.instInhabitedCnstr = { default := { u := default, v := default, k := default } }

def Lean.Meta.Grind.Arith.Offset.Cnstr.neg {α : Type} : Cnstr α → Cnstr α

Equations

• { u := u, v := v, k := k }.neg = { u := v, v := u, k := -k - 1 }

def Lean.Meta.Grind.Arith.Offset.toMessageData {α : Type} [inst : ToMessageData α] (c : Cnstr α) : MessageData

Equations

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

instance Lean.Meta.Grind.Arith.instToMessageDataCnstrExpr : ToMessageData (Offset.Cnstr Expr)

Equations

• Lean.Meta.Grind.Arith.instToMessageDataCnstrExpr = { toMessageData := fun (c : Lean.Meta.Grind.Arith.Offset.Cnstr Lean.Expr) => Lean.Meta.Grind.Arith.Offset.toMessageData c }

def Lean.Meta.Grind.Arith.isNatOffsetCnstr? (e z : Expr) : Option (Offset.Cnstr Expr)

Returns some cnstr if e is offset constraint. Remark: z is 0 numeral. It is an extra argument because we want to be able to provide the one that has already been internalized.

Equations

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

def Lean.Meta.Grind.Arith.isNatOffsetCnstr?.go (z u v : Expr) : Option (Offset.Cnstr Expr)

Equations

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