def Lean.Meta.Grind.Arith.Offset.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.Offset.instToMessageDataCnstrExpr : ToMessageData (Cnstr Expr)

Equations

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

def Lean.Meta.Grind.Arith.Offset.isNatOffsetCnstr? (e z : Expr) : Option (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.Offset.isNatOffsetCnstr?.go (z u v : Expr) : Option (Cnstr Expr)

Equations

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