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

Equations

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

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

Equations

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

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

Equations

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

structure Lean.Meta.Sym.BitVecValue : Type

• n : Nat
• val : BitVec self.n

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

Equations

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

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

Equations

• Lean.Meta.Sym.getUInt8Value? e = do let __do_lift ← Lean.Meta.Sym.getNatValue? e pure (UInt8.ofNat __do_lift)

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

Equations

• Lean.Meta.Sym.getUInt16Value? e = do let __do_lift ← Lean.Meta.Sym.getNatValue? e pure (UInt16.ofNat __do_lift)

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

Equations

• Lean.Meta.Sym.getUInt32Value? e = do let __do_lift ← Lean.Meta.Sym.getNatValue? e pure (UInt32.ofNat __do_lift)

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

Equations

• Lean.Meta.Sym.getUInt64Value? e = do let __do_lift ← Lean.Meta.Sym.getNatValue? e pure (UInt64.ofNat __do_lift)

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

Equations

• Lean.Meta.Sym.getInt8Value? e = do let __do_lift ← Lean.Meta.Sym.getIntValue? e pure (Int8.ofInt __do_lift)

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

Equations

• Lean.Meta.Sym.getInt16Value? e = do let __do_lift ← Lean.Meta.Sym.getIntValue? e pure (Int16.ofInt __do_lift)

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

Equations

• Lean.Meta.Sym.getInt32Value? e = do let __do_lift ← Lean.Meta.Sym.getIntValue? e pure (Int32.ofInt __do_lift)

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

Equations

• Lean.Meta.Sym.getInt64Value? e = do let __do_lift ← Lean.Meta.Sym.getIntValue? e pure (Int64.ofInt __do_lift)

structure Lean.Meta.Sym.FinValue : Type

• n : Nat
• val : Fin self.n

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

Equations

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

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

Equations

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

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

Equations

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