git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4448 from zenntenn/fix/master/difference
fe79d87David Thrane Christiansen
libs/contrib/Data/Nat.idrnew file+8
compare with master
unifiedsplit
@@ -0,0 +1,8 @@
1+module Data.Nat
2+
3+%default total
4+
5+diff : Nat -> Nat -> Nat
6+diff k Z = k
7+diff Z j = j
8+diff (S k) (S j) = diff k j
libs/contrib/contrib.ipkg+1
@@ -43,6 +43,7 @@ modules = CFFI
43 , Data.Matrix.Algebraic
43 , Data.Matrix.Algebraic
44 , Data.Matrix.Numeric
44 , Data.Matrix.Numeric
45
45
46+ , Data.Nat
46 , Data.Nat.Parity
47 , Data.Nat.Parity
47 , Data.Nat.DivMod
48 , Data.Nat.DivMod
48 , Data.Nat.DivMod.IteratedSubtraction
49 , Data.Nat.DivMod.IteratedSubtraction