Почему lean добавляет неявные переменные к леммам из eq?

Question

Следующий код имеет странное поведение

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

Я ожидал бы, что проверка не учитывает не относящуюся к делу неявную переменную toto, показывая мне тип eq.symm. Это действительно предназначено?

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