A value-level representation of a natural number n.
Modulenatural-arithmetic-0.2.4.0Haskell2010
Arithmetic.Types
Contents
Synopsis
- newtype Nat
- newtype Nat#
- data WithNat
- data Difference
- data Fin
- newtype Fin#
- newtype Fin32#
- newtype MaybeFin#
- pattern MaybeFinJust#
- pattern MaybeFinNothing#
- newtype MaybeFin32#
- pattern MaybeFin32Just#
- pattern MaybeFin32Nothing#
- newtype EitherFin#
- pattern EitherFinLeft#
- pattern EitherFinRight#
- data <
- data <=
- newtype <#
- newtype <=#
- data :=:
- newtype :=:#
- Packagenatural-arithmetic-0.2.4.0
- Exports22
- LanguageHaskell2010
- LicenceBSD-3-Clause
- SourceUnsafe.hs
Unboxed variant of Nat.
Proof that the first argument can be expressed as the sum of the second argument and some other natural number.
Constructors
Difference :: Nat c -> (c + b) :=: a -> Difference a b
A finite set of n elements. 'Fin n = { 0 .. n - 1 }'
Finite numbers without the overhead of carrying around a proof.
Variant of Fin# that only allows 32-bit integers.
Maybe Fin
Either a Fin# or Nothing. Internally, this uses negative
one to mean Nothing.
Either Fin
Either a Fin# bounded by the left natural or one bounded
by the right natural.
Infix Operators
Proof that the first argument is strictly less than the second argument.
Proof that the first argument is less than or equal to the second argument.
Proof that the first argument is equal to the second argument.