formal-verification - 为什么精益会在 eq 的引理中添加隐式变量？

Question

以下代码有一个奇怪的行为

variable (toto : Type)
check eq.symm  --output: eq.symm : ?a toto = ?b toto → ?b toto = ?a toto

在向我展示 eq.symm 的类型时，我希望 check 不会考虑不相关的隐式变量 toto。这真的是故意的吗？

Answer 1

我从这里的 github 问题中得到了答案。

这实际上是这里引用的一个错误，可以通过以下方式解决

print eq.symm -- theorem eq.symm : ∀ {A : Type} {a b : A}, a = b → b = a :=
          -- λ A a, eq.rec (eq.refl a)

check @eq.symm -- eq.symm : ∀ {A} {a b}, a = b → b = a