summaryrefslogtreecommitdiff
path: root/src/Data.hs
diff options
context:
space:
mode:
authorTom Smeding <tom@tomsmeding.com>2024-08-30 17:48:15 +0200
committerTom Smeding <tom@tomsmeding.com>2024-08-30 17:48:15 +0200
commit8b047ff11ebd4715647bfc041a190f72dcf4d5a9 (patch)
treee8440120b7bbd4e45b367acb3f7185d25e7f3766 /src/Data.hs
parentf4b94d7cc2cb05611b462ba278e4f12f7a7a5e5e (diff)
Migrate to accumulators (mostly removing EVM code)
Diffstat (limited to 'src/Data.hs')
-rw-r--r--src/Data.hs6
1 files changed, 5 insertions, 1 deletions
diff --git a/src/Data.hs b/src/Data.hs
index 728dafe..c3381d5 100644
--- a/src/Data.hs
+++ b/src/Data.hs
@@ -1,11 +1,11 @@
{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE DeriveTraversable #-}
module Data where
@@ -31,6 +31,10 @@ fromSNat :: SNat n -> Int
fromSNat SZ = 0
fromSNat (SS n) = succ (fromSNat n)
+class KnownNat n where knownNat :: SNat n
+instance KnownNat Z where knownNat = SZ
+instance KnownNat n => KnownNat (S n) where knownNat = SS knownNat
+
data Vec n t where
VNil :: Vec Z t
(:<) :: t -> Vec n t -> Vec (S n) t