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

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

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✝)

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

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

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

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.

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