Coqで型クラスで群論 - Сегодня я узнал

群論に関する定義をするのであれば、型クラスを使うのが一番うまくいくと思います。Class Group G := { gunit : G; gadd : G -> G -> G; ginv : G -> G; gadd_unit_l : forall g : G, gadd g...