Data.Vec.Nat
Description
Type level naturals. Ni is a type, ni an undefined value of that type,
for i <- [0..19]
- 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
- class Pred x y | x -> y, y -> x
Documentation
Instances
| Vec 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)) | |
| 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) |
nat n yields the Int value of the type-level natural n.