Vec-0.9.2: Fixed-length lists and low-dimensional linear algebra. Source code Contents Index

Data.Vec.Nat

Description

Type level naturals. Ni is a type, ni an undefined value of that type, for i <- [0..19]

Synopsis

data N0 data Succ a type N1 = Succ N0 type N2 = Succ N1 type N3 = Succ N2 type N4 = Succ N3 type N5 = Succ N4 type N6 = Succ N5 type N7 = Succ N6 type N8 = Succ N7 type N9 = Succ N8 type N10 = Succ N9 type N11 = Succ N10 type N12 = Succ N11 type N13 = Succ N12 type N14 = Succ N13 type N15 = Succ N14 type N16 = Succ N15 type N17 = Succ N16 type N18 = Succ N17 type N19 = Succ N18 n0 :: N0 n1 :: N1 n2 :: N2 n3 :: N3 n4 :: N4 n5 :: N5 n6 :: N6 n7 :: N7 n8 :: N8 n9 :: N9 n10 :: N10 n11 :: N11 n12 :: N12 n13 :: N13 n14 :: N14 n15 :: N15 n16 :: N16 n17 :: N17 n18 :: N18 n19 :: N19 class Nat n where nat :: n -> Int class Pred x y | x -> y, y -> x

Documentation

data N0 Source

Instances Nat N0 Length () N0 Drop N0 v v Take N0 v () Access N0 a (a :. v) Pred (Succ N0) N0

data Succ a Source

Instances Vec N1 a (a :. ()) Alternating N1 a (a :. ()) Nat a => Nat (Succ a) Pred (Succ N0) N0 Access n a v => Access (Succ n) a (a :. v) Vec (Succ n) a (a' :. v) => Vec (Succ (Succ n)) a (a :. (a' :. v)) (Num a, Alternating n a (a :. v)) => Alternating (Succ n) a (a :. (a :. v)) Pred (Succ n) p => Pred (Succ (Succ n)) (Succ p) (Take (Succ n) v v', PackedVec v, PackedVec v') => Take (Succ n) (Packed v) (Packed v') Drop n (a :. v) v' => Drop (Succ n) (a :. (a :. v)) v' Take n v v' => Take (Succ n) (a :. v) (a :. v') Length v n => Length (a :. v) (Succ n)

type N1 = Succ N0 Source

type N2 = Succ N1 Source

type N3 = Succ N2 Source

type N4 = Succ N3 Source

type N5 = Succ N4 Source

type N6 = Succ N5 Source

type N7 = Succ N6 Source

type N8 = Succ N7 Source

type N9 = Succ N8 Source

type N10 = Succ N9 Source

type N11 = Succ N10 Source

type N12 = Succ N11 Source

type N13 = Succ N12 Source

type N14 = Succ N13 Source

type N15 = Succ N14 Source

type N16 = Succ N15 Source

type N17 = Succ N16 Source

type N18 = Succ N17 Source

type N19 = Succ N18 Source

n0 :: N0 Source

n1 :: N1 Source

n2 :: N2 Source

n3 :: N3 Source

n4 :: N4 Source

n5 :: N5 Source

n6 :: N6 Source

n7 :: N7 Source

n8 :: N8 Source

n9 :: N9 Source

n10 :: N10 Source

n11 :: N11 Source

n12 :: N12 Source

n13 :: N13 Source

n14 :: N14 Source

n15 :: N15 Source

n16 :: N16 Source

n17 :: N17 Source

n18 :: N18 Source

n19 :: N19 Source

class Nat n where Source

nat n yields the Int value of the type-level natural n. Methods nat :: n -> Int Source Instances Nat N0 Nat a => Nat (Succ a)

class Pred x y | x -> y, y -> x Source

Instances Pred (Succ N0) N0 Pred (Succ N0) N0 Pred (Succ n) p => Pred (Succ (Succ n)) (Succ p)

Produced by Haddock version 2.3.0