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

Safe HaskellNone

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) 

class Nat n whereSource

nat n yields the Int value of the type-level natural n.

Methods

nat :: n -> IntSource

Instances

Nat N0 
Nat a => Nat (Succ a) 

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

Instances

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