Entries from 2017-01-01 to 1 day
前回作った俺整数の正しさを証明するために、 俺整数が加法に対してアーベル群をなす事を証明しようと思った。 加法の定義は少し変えた。 module integer4 where import Relation.Binary.PropositionalEquality as PropEq open PropEq using (_≡_; refl; sym…
前回作った俺整数の正しさを証明するために、 俺整数が加法に対してアーベル群をなす事を証明しようと思った。 加法の定義は少し変えた。 module integer4 where import Relation.Binary.PropositionalEquality as PropEq open PropEq using (_≡_; refl; sym…