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 : Lean.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 : Lean.Expr) (typeDeclName : Lake.Name) : Lean.MetaM (Option (Nat × Lean.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 : Lean.Expr) : Lean.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 : Lean.Expr) : Lean.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.getCharValue? (e : Lean.Expr) : Lean.MetaM (Option Char)

Return some c if e is a Char.ofNat-application encoding character c.

Equations

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

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

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

Equations

• Lean.Meta.getStringValue? e = match e with | Lean.Expr.lit (Lean.Literal.strVal s) => some s | x => none

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

Return some ⟨n, v⟩ if e is af 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 : Lean.Expr) : Lean.MetaM (Option ((n : Nat) × BitVec n))

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

Equations

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

def Lean.Meta.getUInt8Value? (e : Lean.Expr) : Lean.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 __discr ← Lean.Meta.getOfNatValue? e `UInt8 match __discr with | (n, snd) => pure (UInt8.ofNat n)).run

def Lean.Meta.getUInt16Value? (e : Lean.Expr) : Lean.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 __discr ← Lean.Meta.getOfNatValue? e `UInt16 match __discr with | (n, snd) => pure (UInt16.ofNat n)).run

def Lean.Meta.getUInt32Value? (e : Lean.Expr) : Lean.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 __discr ← Lean.Meta.getOfNatValue? e `UInt32 match __discr with | (n, snd) => pure (UInt32.ofNat n)).run

def Lean.Meta.getUInt64Value? (e : Lean.Expr) : Lean.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 __discr ← Lean.Meta.getOfNatValue? e `UInt64 match __discr with | (n, snd) => pure (UInt64.ofNat n)).run

def Lean.Meta.normLitValue (e : Lean.Expr) : Lean.MetaM Lean.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 : Lean.Expr) : Lean.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 : Lean.Expr) : Lean.MetaM Lean.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.