Module `Indexing.Sum`

Parameters

module L : CARDINAL

module R : CARDINAL

Signature

type n

val n : n cardinal

val inj_l : L.n index -> n index

val inj_r : R.n index -> n index

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