package fix

You can search for identifiers within the package.

in-package search v0.2.0

Algorithmic building blocks for memoization, recursion, and more

Install

dune-project

Dependency

gitlab.inria.fr Readme Changelog Edit opam file Versions (9)

Authors

F

François Pottier <francois.pottier@inria.fr>

Maintainers

F

francois.pottier@inria.fr

Sources

archive.tar.gz

md5=2a4afa633128c5010677222f7b3c9451

sha512=30d446ba6c19aef78b52d9831eb26f8f6ac10e88bd1eff36d16fbbfb32278b2637e31e63a160aec4abbbfdb1e7612ed25d68c936f4cbf2073e51d713ff3a8adf

doc/fix/Fix/Indexing/Sum/index.html

Module `Indexing.Sum`Source

Sum(L)(R) creates a new type-level set, which is the disjoint sums of the sets L and R. The functor application Sum(L)(R) involves a call to cardinal L.n, thereby fixing the cardinal of the set L, if it was an open-ended set. The cardinal of the set R is not fixed: if R is an open-ended set, then the new set is open-ended as well, and it is still permitted to add new elements to R by calling R.fresh(). Fixing the cardinal of the new set fixes the cardinal of R.

Parameters

module L : CARDINAL

module R : CARDINAL

Signature

include CARDINAL

Sourcetype n

Sourceval n : n cardinal

Sourceval inj_l : L.n index -> n index

Sourceval inj_r : R.n index -> n index

Sourceval prj : n index -> (L.n index, R.n index) either

On This Page

Parameters
Signature