Documentation

Lean.Meta.Tactic.Grind.Arith.Offset.Util

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

An offset constraint.

u : α
v : α
k : Int

Instances For

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 α) :

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.