无法使类型类在Lean中工作

Question

我在理解如何触发Lean的类型类的使用时遇到了麻烦。以下是一个小示例的尝试：

section the_section
structure toto [class] (A : Type) := (rel : A → A → Prop) (Hall : ∀ a, rel a a)

definition P A := exists (a : A), forall x, x = a
parameter A : Type
variable HA : P A

lemma T [instance] {B : Type} [HPB : P B] : toto B := toto.mk (λ x y, x = y) (λ x, rfl)

include HA
example : toto A := _
-- this gives the error: don't know how to infer placeholder toto A

end the_section

重点是我想让Lean看到它可以使用HA从引理T推导出toto A，我错过了什么？

Answer 1

再一次，我不得不张贴这个问题来找到答案。希望这对其他人有帮助。

P需要是一个类，所以我们实际上需要改变

definition P A := exists (a : A), forall x, x = a

至

definition P [class] A := exists (a : A), forall x, x = a