lean

1熱

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 p

formal-methods lean 2016-06-18

---