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_}