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