diff options
Diffstat (limited to 'src/Data.hs')
| -rw-r--r-- | src/Data.hs | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/Data.hs b/src/Data.hs index 0be9046..8005737 100644 --- a/src/Data.hs +++ b/src/Data.hs @@ -77,6 +77,14 @@ fromSNat :: SNat n -> Int fromSNat SZ = 0 fromSNat (SS n) = succ (fromSNat n) +unSNat :: SNat n -> Nat +unSNat SZ = Z +unSNat (SS n) = S (unSNat n) + +fromNat :: Nat -> Int +fromNat Z = 0 +fromNat (S m) = succ (fromNat m) + class KnownNat n where knownNat :: SNat n instance KnownNat Z where knownNat = SZ instance KnownNat n => KnownNat (S n) where knownNat = SS knownNat @@ -124,6 +132,7 @@ unsafeCoerceRefl = unsafeCoerce Refl data Bag t = BNone | BOne t | BTwo (Bag t) (Bag t) | BMany [Bag t] deriving (Show, Functor, Foldable, Traversable) +-- | This instance is mostly there just for 'pure' instance Applicative Bag where pure = BOne BNone <*> _ = BNone |