Mercurial > hg > Papers > 2021 > soto-thesis
view paper/src/AgdaInstance.agda.replaced @ 14:a63df15c9afc default tip
DONE
author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 15 Feb 2021 23:36:39 +0900 (2021-02-15) |
parents | 959f4b34d6f4 |
children |
line wrap: on
line source
_==Nat_ : Nat @$\rightarrow$@ Nat @$\rightarrow$@ Bool zero ==Nat zero = true (suc n) ==Nat zero = false zero ==Nat (suc m) = false (suc n) ==Nat (suc m) = n ==Nat m instance natHas== : Eq Nat natHas== = record { _==_ = _==Nat_}