Finds the difference between two Nats
new file: libs/contrib/Data/Nat/Difference.idr
commitd3badf2905a79e7c28785541c8abb75e8bee9a32
authorzenntenn <zenten@zenten.ca>
dateMon 21 May 2018, 14:17 (8 years ago)
parent88f5c71
libs/contrib/Data/Nat/Difference.idrnew file+6
@@ -0,0 +1,6 @@
1+%default total
2+
3+diff : Nat -> Nat -> Nat
4+diff k Z = k
5+diff Z j = j
6+diff (S k) (S j) = diff k j