package fix

  1. Overview
  2. Docs

Module type Indexing.SUMSource

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