package fix

  1. Overview
  2. Docs
Algorithmic building blocks for memoization, recursion, and more

Install 

dune-project
 Dependency

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

Authors

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

Maintainers

  1. F
    francois.pottier@inria.fr

Sources

archive.tar.gz
md5=2a4afa633128c5010677222f7b3c9451
sha512=30d446ba6c19aef78b52d9831eb26f8f6ac10e88bd1eff36d16fbbfb32278b2637e31e63a160aec4abbbfdb1e7612ed25d68c936f4cbf2073e51d713ff3a8adf

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

Module Indexing.SumSource

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 inj_l : L.n index -> n index
Sourceval inj_r : R.n index -> n index