vector-static-0.0.1: 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

Constructors Z Instances Nat Z

newtype S n Source

Constructors S n Instances Nat n => Nat (S n)

class Nat n where Source

Methods caseNat :: forall r. n -> (n ~ Z => r) -> (forall p. (n ~ S p, Nat p) => p -> r) -> r Source Instances Nat Z Nat n => Nat (S n)

induction :: forall p n. Nat n => n -> p Z -> (forall x. Nat x => p x -> p (S x)) -> p n Source

natToInt :: Nat n => n -> Int Source

witnessNat :: forall n. Nat n => n Source

type family a :+: b :: * Source

type family a :*: b :: * Source

Produced by Haddock version 2.6.0