Vec-0.9.0: Fixed-length lists and low-dimensional linear algebra.Source codeContentsIndex
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
show/hide Instances
Nat N0
Drop N0 v v
Take N0 v ()
Access N0 a (a :. v)
Pred (Succ N0) N0
data Succ a Source
show/hide Instances
Vec N1 a (a :. ())
Alternating N1 a (a :. ())
Nat a => Nat (Succ a)
Pred (Succ N0) N0
(Tail v' v'', Drop n v v') => Drop (Succ n) v v''
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 n v v' => Take (Succ n) (a :. v) (a :. v')
type N1 = Succ N0Source
type N2 = Succ N1Source
type N3 = Succ N2Source
type N4 = Succ N3Source
type N5 = Succ N4Source
type N6 = Succ N5Source
type N7 = Succ N6Source
type N8 = Succ N7Source
type N9 = Succ N8Source
type N10 = Succ N9Source
type N11 = Succ N10Source
type N12 = Succ N11Source
type N13 = Succ N12Source
type N14 = Succ N13Source
type N15 = Succ N14Source
type N16 = Succ N15Source
type N17 = Succ N16Source
type N18 = Succ N17Source
type N19 = Succ N18Source
n0 :: N0Source
n1 :: N1Source
n2 :: N2Source
n3 :: N3Source
n4 :: N4Source
n5 :: N5Source
n6 :: N6Source
n7 :: N7Source
n8 :: N8Source
n9 :: N9Source
n10 :: N10Source
n11 :: N11Source
n12 :: N12Source
n13 :: N13Source
n14 :: N14Source
n15 :: N15Source
n16 :: N16Source
n17 :: N17Source
n18 :: N18Source
n19 :: N19Source
class Nat n whereSource
nat n yields the Int value of the type-level natural n.
Methods
nat :: n -> IntSource
show/hide Instances
Nat N0
Nat a => Nat (Succ a)
class Pred x y | x -> y, y -> xSource
show/hide 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