Agdaで俺整数を定義してみた。 Natから符号を付けてIntを定義する方法も考えたけど、ゴチャゴチャしてやめた。 0と、+1を表すPと、-1を表すMで構成した。 module integer2 where import Relation.Binary.PropositionalEquality as PropEq open PropEq using …