Module type `Indexing.SUM`

The signature SUM extends CARDINAL with an explicit isomorphism between the set n and the disjoint sum l + r. The functions inj_l and inj_r convert an index into l or an index into r into an index into n. Conversely, the function prj converts an index into r into either an index into l or an index into r.

type l

and r

include CARDINAL

type n

val n : n cardinal

val inj_l : l index -> n index

val inj_r : r index -> n index

val prj : n index -> (l index, r index) either