1 files changed, 15 insertions, 0 deletions
diff --git a/src/Data.hs b/src/Data.hs
index eb6c033..840cb88 100644
--- a/src/Data.hs
+++ b/src/Data.hs
@@ -9,9 +9,15 @@
 {-# LANGUAGE TypeOperators #-}
 module Data where
 
+import Data.Type.Equality
+
 import Lemmas (Append)
 
 
+data Dict c where
+  Dict :: c => Dict c
+
+
 data SList f l where
   SNil :: SList f '[]
   SCons :: f a -> SList f l -> SList f (a : l)
@@ -42,6 +48,11 @@ data SNat n where
   SS :: SNat n -> SNat (S n)
 deriving instance Show (SNat n)
 
+instance TestEquality SNat where
+  testEquality SZ SZ = Just Refl
+  testEquality (SS n) (SS n') | Just Refl <- testEquality n n' = Just Refl
+  testEquality _ _ = Nothing
+
 fromSNat :: SNat n -> Int
 fromSNat SZ = 0
 fromSNat (SS n) = succ (fromSNat n)
@@ -50,6 +61,10 @@ class KnownNat n where knownNat :: SNat n
 instance KnownNat Z where knownNat = SZ
 instance KnownNat n => KnownNat (S n) where knownNat = SS knownNat
 
+snatKnown :: SNat n -> Dict (KnownNat n)
+snatKnown SZ = Dict
+snatKnown (SS n) | Dict <- snatKnown n = Dict
+
 data Vec n t where
   VNil :: Vec Z t
   (:<) :: t -> Vec n t -> Vec (S n) t