git.iko.soy/type-fun
on master help sign in
KnownPeano
commit3d4e50b2d3862371579a159ab7d1cd207113328f authorAleksey Uymanov <s9gf4ult@gmail.com> dateSun 11 Oct 2020, 21:55 (6 years ago) parentfe5ca13
3 files changed+30
compare with master
unifiedsplit
src/TypeFun/Data/Peano.hs+9 stack.yaml+9 stack.yaml.lock+12
src/TypeFun/Data/Peano.hs+9
@@ -15,6 +15,15 @@ data N = Z | S N
1515 deriving ( Eq, Ord, Read, Show
1616 , Generic, Typeable )
1717
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+
1827type family ToNat (a :: N) :: Nat where
1928 ToNat Z = 0
2029 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