lean - 为什么要同时使用类型类和隐式参数机制？

Question

所以我们可以有明确的参数，用 表示()。
我们也可以有隐式参数，用 表示{}。

到目前为止，一切都很好。

但是，为什么我们还需要[]专门针对类型类的符号呢？

以下两者有什么区别：

theorem foo  {x : Type} : ∀s : inhabited x, x := sorry
theorem foo' {x : Type} [s : inhabited x] : x := sorry

Answer 1

Lean 的阐述器会自动插入隐式参数。您的{x : Type}两个定义中出现的 是隐式参数的一个示例：如果您有s : inhabited nat，那么您可以编写foo s，这将详细说明为 type 的术语nat，因为x可以从 推断出参数s。

类型类参数是另一种隐式参数。阐述器不是从后面的参数中推断出来的，而是运行一个称为类型类解析的过程，该过程将尝试生成指定类型的术语。（请参阅https://leanprover.github.io/theorem_proving_in_lean/theorem_proving_in_lean.pdf的第 10 章。）因此，您foo'实际上根本不会接受任何论点。x如果可以从上下文中推断出预期的类型，Lean 将查找inhabited x并插入它的实例：

def foo' {x : Type} [s : inhabited x] : x := default x
instance inh_nat : inhabited nat := ⟨3⟩
#eval (2 : ℕ) + foo' -- 5

在这里，Lean 推断出x必须是nat，并找到并插入 的实例inhabited nat，因此foo'仅此一项就可以解释为类型 的术语nat。