vector-static-0.1.2: 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
::
Nat
x ->
Fin
(
S
y) ->
Fin
(
S
(x
:*:
y))
Source
raise
:: k ->
Fin
n ->
Fin
(n
:+:
k)
Source
intToFin
::
Int
->
Nat
n ->
Maybe
(
Fin
n)
Source
finToInt
::
Fin
n ->
Int
Source
natToFin
::
Nat
n ->
Fin
(
S
n)
Source
Produced by
Haddock
version 2.6.0