Lean为何允许无效UInt8字面量？编译运行行为及写法咨询

为什么(0xFFFF : UInt8)能编译通过？ #

这不是疏漏，而是Lean的设计选择。Lean虽然重视正确性证明，但并未默认禁止所有可能产生“意外”的数值转换——系统编程、底层开发场景中，数值截断是常见且必要的操作。Lean的核心是让你可以证明程序行为符合预期，而非替你屏蔽所有潜在操作：若需确保转换无截断，你可以编写定理证明数值在UInt8范围内；若明确需要截断行为，直接做类型转换即可，Lean允许这种显式操作。

运行时表现 #

0xFFFF对应十进制65535，转换为UInt8时会自动截断到低8位，最终x的运行时值为0xFF（即十进制255）。

更优雅的UInt8字面量写法 #

Lean默认支持直接给字面量加类型标注，写法0xFF : UInt8已足够简洁。如果想要类似Rust的0xFFu8后缀写法，可以自定义notation：

notation:max n:max "u8" => n : UInt8

定义后即可直接写0xFFu8，效果和0xFF : UInt8完全一致。

内容的提问来源于stack exchange，提问作者Timmmm