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

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

Increments the constant part of the offset by k'.

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.

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

Returns true if e is an offset term.

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.

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

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

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