Mercurial > hg > Papers > 2020 > ryokka-master
view paper/src/agda-pattern.agda.replaced @ 7:8ef64db63497
fix agda.tex
author | ryokka |
---|---|
date | Thu, 06 Feb 2020 19:24:32 +0900 |
parents | |
children | 831316a767e8 |
line wrap: on
line source
_-_ : Nat @$\rightarrow$@ Nat @$\rightarrow$@ Nat n - zero = n -- "n - zero" have 2-pattern, "zero - zero" "suc n - zero" zero - suc m = zero suc n - suc m = n - m