vector-static-0.3.0: Statically checked sizes on Data.Vector
Source code
Contents
Index
Data.Fin
Documentation
newtype
Fin
n
Source
Constructors
Fin
Int
Instances
Vector
v
Int
=>
Vector
v (
Fin
n)
MVector
v
Int
=>
MVector
v (
Fin
n)
Eq
(
Fin
n)
Ord
(
Fin
n)
Show
(
Fin
n)
Unbox
(
Fin
n)
zero
::
Fin
(
S
n)
Source
succ
::
Fin
n ->
Fin
(
S
n)
Source
pred
::
Fin
n ->
Fin
n
Source
addFin
::
Fin
x ->
Fin
y ->
Fin
(x
:+:
y)
Source
mulFin
::
Fin
x ->
Fin
y ->
Fin
(x
:*:
y)
Source
mulNatFin
::
forall
x y.
Reify
x =>
Fin
(
S
y) ->
Fin
(
S
(x
:*:
y))
Source
raise
::
Fin
n ->
Fin
(n
:+:
k)
Source
intToFin
::
forall
n.
Reify
n =>
Int
->
Maybe
(
Fin
n)
Source
finToInt
::
Fin
n ->
Int
Source
natToFin
::
forall
n.
Reify
n =>
Fin
(
S
n)
Source
Produced by
Haddock
version 2.6.0