유형 클래스가 약식으로 작동하지 못함

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.에서 토토 A를 추론 할 HA를 사용할 수있는 볼 린하고자한다 : 여기에 작은 예제를 시도인가?

Answer 1

다시 한번 대답을 찾으려면 질문을 게시해야했습니다. 희망이 다른 사람들에게 도움이됩니다.

P는 클래스가 될 필요가있다, 그래서 우리는 실제로

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

에

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

을 변경해야