vector-static-0.3.0.1: Statically checked sizes on Data.Vector
Data.Nat
newtype I x Source
Constructors
Fields
newtype K x y Source
data Z Source
Instances
data S n Source
newtype Nat n Source
z :: Nat ZSource
s :: Nat n -> Nat (S n)Source
natToInt :: Nat n -> IntSource
data Reifiable n whereSource
data Exists Source
reifiable :: Nat n -> Reifiable nSource
class Reify n whereSource
Methods
witnessNat :: Nat nSource
type family a :+: b :: *Source
type family a :*: b :: *Source
addNat :: Nat a -> Nat b -> Nat (a :+: b)Source
mulNat :: Nat a -> Nat b -> Nat (a :*: b)Source
data NatView n whereSource
view :: Nat n -> NatView nSource