vector-static-0.3.0.1: Statically checked sizes on Data.Vector

Data.Nat

Documentation

newtype I x Source

Constructors

I 

Fields

unI :: x
 

newtype K x y Source

Constructors

K 

Fields

unK :: x
 

data Z Source

Instances

data S n Source

Instances

Reify n => Reify (S n) 

newtype Nat n Source

Constructors

Nat Int 

Instances

Show (Nat n) 

s :: Nat n -> Nat (S n)Source

data Reifiable n whereSource

Constructors

Proof :: Reify n => Reifiable n 

data Exists Source

Constructors

forall n . Ex !(Reifiable n) 

class Reify n whereSource

Methods

witnessNat :: Nat nSource

Instances

Reify Z 
Reify n => Reify (S n) 

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

Constructors

Zero :: NatView Z 
Succ :: Nat n -> NatView (S n)