Невозможно заставить классы классов работать в 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 вывести Toto А из леммы Т. Что мне не хватает?

Answer 1

Еще раз, я должен был поставить вопрос, чтобы найти ответ. Надеюсь, это поможет другим людям.

P должен быть классом, так что мы на самом деле нужно изменить

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

в

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