タイプクラスがリーンで動作しない

Question

リーンでタイプクラスの使用をトリガーする方法を理解できません。ここで小さな例の試みです：

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 

ポイントは、私はそれが私が行方不明です何補題T.からTOTOのAを推定するためにHAを使用することができることを見ることがリーンたいのですか？

Answer 1

もう一度、回答を見つけるために質問を投稿する必要がありました。これが他の人に役立つことを望みます。

Pは、クラスにする必要があるので、我々は実際に

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

に

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

を変更する必要があります