Helper functions for recognizing builtin literal values. This module focus on recognizing the standard representation used in Lean for these literals. It also provides support for the following exceptional cases.

• Raw natural numbers (i.e., natural numbers which are not encoded using OfNat.ofNat).
• Bit-vectors encoded using OfNat.ofNat and BitVec.ofNat.
• Negative integers encoded using raw natural numbers.
• Characters encoded Char.ofNat n where n can be a raw natural number or an OfNat.ofNat.
• Nested Expr.mdata.

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

Returns some n if e is a raw natural number, i.e., it is of the form .lit (.natVal n).

Equations

• Lean.Meta.getRawNatValue? e = match e.consumeMData with | Lean.Expr.lit (Lean.Literal.natVal n) => some n | x => none

def Lean.Meta.getOfNatValue? (e : Expr) (typeDeclName : Name) : MetaM (Option (Nat × Expr))

Return some (n, type) if e is an OfNat.ofNat-application encoding n for a type with name typeDeclName.

Equations

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

def Lean.Meta.getNatValue? (e : Expr) : MetaM (Option Nat)

Return some n if e is a raw natural number or an OfNat.ofNat-application encoding n.

Equations

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

def Lean.Meta.getIntValue? (e : Expr) : MetaM (Option Int)

Return some i if e OfNat.ofNat-application encoding an integer, or Neg.neg-application of one.

Equations

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

def Lean.Meta.getRatValue? (e : Expr) : MetaM (Option Rat)

Return some i if e OfNat.ofNat-application encoding a rational, or Neg.neg-application of one, or a division.

Equations

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

def Lean.Meta.getCharValue? (e : Expr) : MetaM (Option Char)

Return some c if e is a Char.ofNat-application that encodes the character c.

Equations

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

def Lean.Meta.getStringValue? (e : Expr) : Option String

Return some s if e is of the form .lit (.strVal s).

Equations

• Lean.Meta.getStringValue? (Lean.Expr.lit (Lean.Literal.strVal s)) = some s
• Lean.Meta.getStringValue? e = none

def Lean.Meta.getFinValue? (e : Expr) : MetaM (Option ((n : Nat) × Fin n))

Return some ⟨n, v⟩ if e is an OfNat.ofNat application encoding a Fin n with value v

Equations

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

def Lean.Meta.getBitVecValue? (e : Expr) : MetaM (Option ((n : Nat) × BitVec n))

Return some ⟨n, v⟩ if e is:

• an OfNat.ofNat application
• a BitVec.ofNat application
• a BitVec.ofNatLT application that encode a BitVec n with value v.

Equations

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

def Lean.Meta.getLitValueModulus? (α : Expr) : MetaM (Option Nat)

Returns the modulus of the wrapping numeric type α (n for Fin n, 2^w for the fixed-width types) if it is known. USize/ISize are not included: their widths are platform-dependent.

Equations

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

def Lean.Meta.getUInt8Value? (e : Expr) : MetaM (Option UInt8)

Return some n if e is an OfNat.ofNat-application encoding the UInt8 with value n.

Equations

• Lean.Meta.getUInt8Value? e = (do let __x ← Lean.Meta.getOfNatValue? e `UInt8 match __x with | (n, snd) => pure (UInt8.ofNat n)).run

def Lean.Meta.getUInt16Value? (e : Expr) : MetaM (Option UInt16)

Return some n if e is an OfNat.ofNat-application encoding the UInt16 with value n.

Equations

• Lean.Meta.getUInt16Value? e = (do let __x ← Lean.Meta.getOfNatValue? e `UInt16 match __x with | (n, snd) => pure (UInt16.ofNat n)).run

def Lean.Meta.getUInt32Value? (e : Expr) : MetaM (Option UInt32)

Return some n if e is an OfNat.ofNat-application encoding the UInt32 with value n.

Equations

• Lean.Meta.getUInt32Value? e = (do let __x ← Lean.Meta.getOfNatValue? e `UInt32 match __x with | (n, snd) => pure (UInt32.ofNat n)).run

def Lean.Meta.getUInt64Value? (e : Expr) : MetaM (Option UInt64)

Return some n if e is an OfNat.ofNat-application encoding the UInt64 with value n.

Equations

• Lean.Meta.getUInt64Value? e = (do let __x ← Lean.Meta.getOfNatValue? e `UInt64 match __x with | (n, snd) => pure (UInt64.ofNat n)).run

def Lean.Meta.getFloatValue? (e : Expr) : MetaM (Option Float)

Return some v if e is a Float literal: an OfScientific or OfNat application, or Neg.neg of either (e.g. -1.5).

Equations

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

def Lean.Meta.getFloat32Value? (e : Expr) : MetaM (Option Float32)

Return some v if e is a Float32 literal: an OfScientific or OfNat application, or Neg.neg of either (e.g. -1.5).

Equations

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

def Lean.Meta.normLitValue (e : Expr) : MetaM Expr

If e is a literal value, ensure it is encoded using the standard representation. Otherwise, just return e.

Equations

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

def Lean.Meta.isLitValue (e : Expr) : MetaM Bool

Returns true if e is a literal value.

Equations

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

def Lean.Meta.litToCtor (e : Expr) : MetaM Expr

If e is a Nat, Int, or Fin literal value, converts it into a constructor application. Otherwise, just return e.

Equations

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

def Lean.Meta.getListLitOf? {α : Type} (e : Expr) (f : Expr → MetaM (Option α)) : MetaM (Option (Array α))

Check if an expression is a list literal (i.e. a nested chain of List.cons, ending at a List.nil), where each element is "recognised" by a given function f : Expr → MetaM (Option α), and return the array of recognised values.

Equations

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

def Lean.Meta.getListLit? (e : Expr) : MetaM (Option (Array Expr))

Check if an expression is a list literal (i.e. a nested chain of List.cons, ending at a List.nil), returning the array of Expr values.

Equations

• Lean.Meta.getListLit? e = Lean.Meta.getListLitOf? e fun (s : Lean.Expr) => pure (some s)

def Lean.Meta.getArrayLitOf? {α : Type} (e : Expr) (f : Expr → MetaM (Option α)) : MetaM (Option (Array α))

Check if an expression is an array literal (i.e. List.toArray applied to a nested chain of List.cons, ending at a List.nil), where each element is "recognised" by a given function f : Expr → MetaM (Option α), and return the array of recognised values.

Equations

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

def Lean.Meta.getArrayLit? (e : Expr) : MetaM (Option (Array Expr))

Check if an expression is an array literal (i.e. List.toArray applied to a nested chain of List.cons, ending at a List.nil), returning the array of Expr values.

Equations

• Lean.Meta.getArrayLit? e = Lean.Meta.getArrayLitOf? e fun (s : Lean.Expr) => pure (some s)