Pure functions for extracting values. They are pure (OptionT Id) rather than monadic (MetaM). This is possible because Sym assumes terms are in canonical form, no whnf or reduction is needed to recognize literals.

def Lean.Meta.Sym.getNatValue? (e : Expr) : OptionT Id Nat

def Lean.Meta.Sym.getIntValue? (e : Expr) : OptionT Id Int

def Lean.Meta.Sym.getRatValue? (e : Expr) : OptionT Id Rat

structure Lean.Meta.Sym.BitVecValue : Type

• n : Nat
• val : BitVec self.n

def Lean.Meta.Sym.getBitVecValue? (e : Expr) : OptionT Id BitVecValue

def Lean.Meta.Sym.getUInt8Value? (e : Expr) : OptionT Id UInt8

def Lean.Meta.Sym.getUInt16Value? (e : Expr) : OptionT Id UInt16

def Lean.Meta.Sym.getUInt32Value? (e : Expr) : OptionT Id UInt32

def Lean.Meta.Sym.getUInt64Value? (e : Expr) : OptionT Id UInt64

def Lean.Meta.Sym.getInt8Value? (e : Expr) : OptionT Id Int8

def Lean.Meta.Sym.getInt16Value? (e : Expr) : OptionT Id Int16

def Lean.Meta.Sym.getInt32Value? (e : Expr) : OptionT Id Int32

def Lean.Meta.Sym.getInt64Value? (e : Expr) : OptionT Id Int64

structure Lean.Meta.Sym.FinValue : Type

• n : Nat
• val : Fin self.n

def Lean.Meta.Sym.getFinValue? (e : Expr) : OptionT Id FinValue

def Lean.Meta.Sym.getCharValue? (e : Expr) : OptionT Id Char

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