git.iko.soy/type-fun
on master help sign in
KnownPeano
3d4e50bAleksey Uymanov
src/TypeFun/Data/Peano.hs+9
compare with master
unifiedsplit
@@ -15,6 +15,15 @@ data N = Z | S N
15 deriving ( Eq, Ord, Read, Show
15 deriving ( Eq, Ord, Read, Show
16 , Generic, Typeable )
16 , Generic, Typeable )
17
17
18+class KnownPeano (p :: N) where
19+ peanoVal :: proxy p -> Integer
20+
21+instance KnownPeano Z where
22+ peanoVal _ = 0
23+
24+instance (KnownPeano n) => KnownPeano (S n) where
25+ peanoVal _ = succ $ peanoVal (Proxy :: Proxy n)
26+
18type family ToNat (a :: N) :: Nat where
27type family ToNat (a :: N) :: Nat where
19 ToNat Z = 0
28 ToNat Z = 0
20 ToNat (S a) = 1 + (ToNat a)
29 ToNat (S a) = 1 + (ToNat a)
stack.yamlnew file+9
@@ -0,0 +1,9 @@
1+nix:
2+ packages:
3+ - zlib
4+ - postgresql
5+
6+resolver: lts-13.21
7+
8+packages:
9+ - .
stack.yaml.locknew file+12
@@ -0,0 +1,12 @@
1+# This file was autogenerated by Stack.
2+# You should not edit this file by hand.
3+# For more information, please see the documentation at:
4+# https://docs.haskellstack.org/en/stable/lock_files
5+
6+packages: []
7+snapshots:
8+- completed:
9+ size: 498180
10+ url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/13/21.yaml
11+ sha256: eff2de19a6d4691ccbf6edc1fba858f1918683047dce0f09adede874bbd2a8f3
12+ original: lts-13.21