vector-static-0.2.0: Statically checked sizes on Data.Vector Source code Contents Index

Data.Nat

Documentation

newtype I x Source

Constructors I unI :: x

newtype K x y Source

Constructors K unK :: x

data Z Source

Instances Reify Z

data S n Source

Instances Reify n => Reify (S n)

newtype Nat n Source

Constructors Nat Int Instances Show (Nat n)

z :: Nat Z Source

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

natToInt :: Nat n -> Int Source

data Reifiable n where Source

Constructors Proof :: Reify n => Reifiable n

data Exists Source

Constructors forall n . Ex !(Reifiable n)

reifiable :: Nat n -> Reifiable n Source

class Reify n where Source

Methods witnessNat :: Nat n Source 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 where Source

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

view :: Nat n -> NatView n Source

Produced by Haddock version 2.6.0