1
我無法理解如何觸發精益類型類的使用。這裏是一個小例子，企圖：不能讓類型類在精益中工作
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
關鍵是我想精益看到，它可以使用HA來推斷從引理T. TOTO一個我缺少什麼？