非安全（unsafe）声明

Lean 的表层语言允许用户编写带有 unsafe 标记的声明，这类声明能执行通常被禁止的操作。例如，Lean 接受下面的定义：

unsafe def y : Nat := y

非安全声明不会被导出 ¹，因此也无需被信任；并且，即便在表层语言里，它们也不能出现在正式证明中。之所以仍允许写 unsafe 声明，是为了让用户在编写 生成证明的辅助代码（本身不一定是证明）时拥有更大的自由度。

aesop 库提供了一个现实范例。Aesop 是一个自动化框架，用来帮助用户生成证明。开发过程中，作者发现用 互递归归纳类型 表达系统的某部分最合适，代码见此。但这一组归纳类型在 Lean 理论里存在不合法的自引用，不会被内核接受，因此必须标记为 unsafe。

允许将该定义作 unsafe 声明是一种双赢：Aesop 开发者得以继续在 Lean 中用熟悉的语法实现库，而无需另学一套元编程 DSL，也不必为取悦内核大费周章；而 Aesop 的使用者仍能导出并验证 Aesop 生成的 证明，而无需验证 Aesop 自身。