git.iko.soy/Idris-dev
on master help sign in
Finds the difference between two Nats
d3badf2zenntenn
libs/contrib/Data/Nat/Difference.idrnew file+6
compare with master
unifiedsplit
@@ -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