Vec-1.0.5: Fixed-length lists and low-dimensional linear algebra.

Data.Vec.Nat

Description

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

Synopsis

# Documentation

data N0 Source

Instances

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

data Succ a Source

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)

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

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 n) p => Pred (Succ (Succ n)) (Succ p)