数值字面量分为两类：自然数字面量和科学计数字面量。 二者都通过类型类重载。
自然数可以用以下几种形式指定：
由数字 0 至 9 组成的序列是十进制字面量
0b 或 0B 后跟由一个或多个 0 与 1 组成的序列，是二进制字面量
0o 或 0O 后跟由一个或多个 0 至 7 的数字组成的序列，是八进制字面量
0x 或 0X 后跟由一个或多个十六进制数字（0 至 9 以及 A 至 F，不区分大小写）组成的序列，是十六进制字面量
所有数值字面量内部都可以包含下划线，但二进制、八进制或十六进制字面量的前两个字符之间除外。
这些下划线旨在帮助以自然方式对数字分组，例如 1_000_000 或 0x_c0de_cafe。
（虽然可以将数字 123 写成 1_2__3，但不推荐这样做。）
Lean 遇到自然数字面量 n 时，会通过重载方法 OfNat.ofNat n 解释它。
OfNat Nat n 的一个默认实例确保在没有其他类型信息时可以推断出类型 Nat。
自然数字面量的重载接口。
例如，表达式 37 : α 会触发 OfNat α 37 的实例合成，并被精译为
(OfNat.ofNat 37 : α)。严格地说，原始自然数字面量由项构造子 nat_lit 表示；
它们始终具有类型 Nat，因此生成的项不会在参数外再套一层 OfNat.ofNat。
实例构造子
OfNat.mk.{u}
方法
ofNat : α
用户写下 1 : α 之类的数值字面量时，解析器会自动插入 OfNat.ofNat。
因而，类型类实例可以根据自然数值及目标类型 α 自定义字面量的含义。
结构 NatInterval 表示一个自然数区间。
structure NatInterval where
low : Nat
high : Nat
low_le_high : low ≤ high
instance : Add NatInterval where
add
| ⟨lo1, hi1, le1⟩, ⟨lo2, hi2, le2⟩ =>
⟨lo1 + lo2, hi1 + hi2, lo1:Nathi1:Natle1:lo1 ≤ hi1lo2:Nathi2:Natle2:lo2 ≤ hi2⊢ lo1 + lo2 ≤ hi1 + hi2 All goals completed! 🐙⟩
OfNat 实例使自然数字面量可以用来表示区间：
instance : OfNat NatInterval n where
ofNat := ⟨n, n, n:Nat⊢ n ≤ n All goals completed! 🐙⟩
#eval (8 : NatInterval)
#eval (0b111 : NatInterval)
并没有单独的整数字面量。
-5 这样的项由应用于自然数字面量的前缀取负操作构成（它可以通过 Neg 类型类重载）。
科学计数字面量由一个十进制数字序列、一个可选的小数部分（句点后跟零个或多个十进制数字）和一个可选的指数部分（字母 e 后跟可选的 + 或 -，再跟一个或多个十进制数字）组成，各部分之间不能有空白。
科学计数字面量通过 OfScientific 类型类重载。
十进制及科学计数字面量（例如 1.23、3.12e10）的重载接口。
示例：
1.23 是 OfScientific.ofScientific (nat_lit 123) true (nat_lit 2) 的语法糖；
121e100 是 OfScientific.ofScientific (nat_lit 121) false (nat_lit 100) 的语法糖。
这里使用原始自然数字面量 nat_lit；生成的项不会再套一层 OfNat.ofNat。
实例构造子
OfScientific.mk.{u}
方法
ofScientific : Nat → Bool → Nat → α
根据给定的尾数、指数符号和十进制指数生成一个值。指数符号为 true 时表示负指数。
示例：
1.23 是 OfScientific.ofScientific (nat_lit 123) true (nat_lit 2) 的语法糖；
121e100 是 OfScientific.ofScientific (nat_lit 121) false (nat_lit 100) 的语法糖。
这里使用原始自然数字面量 nat_lit；生成的项不会再套一层 OfNat.ofNat。
存在用于 Float 和 Float32 的 OfScientific 实例，但不存在单独的浮点字面量。
字符串字面量在关于字符串的章节中介绍。
列表和数组字面量是在方括号内以逗号分隔的元素序列，数组的方括号前还带有井号（#）。
数组字面量会被解释为由转换调用包裹的列表字面量。
出于性能考虑，非常长的列表和数组字面量会被转换为一系列局部定义，而不仅仅是列表构造器的迭代应用。
term ::= ...
| term ::= ...
|