On Mar 15, 2014, at 4:48 PM, Henning Thielemann wrote:
What is the meaning of KnownNat?
It is a Nat whose value is known at runtime. I'll confess to suggesting the
name… I think I was hoping there would be more debate and a better idea at the
time, but it just stuck.
I see that there is no
To answer your second question using GADT-style vectors:
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators#-}
{-# LANGUAGE ScopedTypeVariables #-}
module WithVector where
import Data.Maybe
import Data.Proxy
