Offset representation for natural number expressions

This module provides utilities for representing Nat expressions in the form e + k, where e is an arbitrary expression and k is a constant. This normalization is used during pattern matching and unification.

inductive Lean.Meta.Sym.Offset : Type

Represents a natural number expression as a base plus a constant offset.

• .num k represents the literal k
• .add e k represents e + k

Used for pattern matching and unification.

• num (k : Nat) : Offset
• add (e : Expr) (k : Nat) : Offset

@[instance_reducible]

instance Lean.Meta.Sym.instInhabitedOffset : Inhabited Offset

Equations

• Lean.Meta.Sym.instInhabitedOffset = { default := Lean.Meta.Sym.instInhabitedOffset.default }

def Lean.Meta.Sym.Offset.inc : Offset → Nat → Offset

Increments the constant part of the offset by k'.

Equations

• (Lean.Meta.Sym.Offset.num k).inc x✝ = Lean.Meta.Sym.Offset.num (k + x✝)
• (Lean.Meta.Sym.Offset.add e k).inc x✝ = Lean.Meta.Sym.Offset.add e (k + x✝)

partial def Lean.Meta.Sym.isOffset? (e : Expr) : OptionT Id Offset

Returns some offset if e is an offset term. That is, it is of the form

• Nat.succ a, OR
• a + k where k is a numeral.

Assumption: standard instances are used for OfNat Nat n and HAdd Nat Nat Nat

def Lean.Meta.Sym.isOffset?' (declName : Name) (p : Expr) : OptionT Id Offset

Variant of isOffset? that first checks if declName is Nat.succ or HAdd.hAdd.

Equations

• Lean.Meta.Sym.isOffset?' declName p = do guard ((declName == `Nat.succ || declName == `HAdd.hAdd) = true) Lean.Meta.Sym.isOffset? p

def Lean.Meta.Sym.isOffset (e : Expr) : Bool

Returns true if e is an offset term.

Equations

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

def Lean.Meta.Sym.isQuasiOffset (p : Expr) : Bool

Returns true if the pattern p is a + k over Nat where k contains pattern variables. Once the pattern variables are instantiated, such a subterm may match a numeral or an offset (e.g. ?m + ?n =?= 16 with ?m := 8, ?n := 8), so it must be indexed as a wildcard. See isQuasiOffsetCnstr.

Equations

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

def Lean.Meta.Sym.isOffset' (declName : Name) (p : Expr) : Bool

Variant of isOffset? that first checks if declName is Nat.succ or HAdd.hAdd.

Equations

• Lean.Meta.Sym.isOffset' declName p = ((declName == `Nat.succ || declName == `HAdd.hAdd) && Lean.Meta.Sym.isOffset p)

partial def Lean.Meta.Sym.toOffset (e : Expr) : Offset

Converts the given expression into an offset. Assumptions:

• e has type Nat.
• standard instances are used for OfNat Nat n and HAdd Nat Nat Nat.

def Lean.Meta.Sym.isNatValue? (e : Expr) : Option Nat

Equations

• Lean.Meta.Sym.isNatValue? e = if Lean.Meta.Sym.isNatExpr✝ e = true then Lean.Meta.Sym.evalNat?✝ e else none