Module KTDeque.Coq_ESource

Sourcetype 'a t = (int, 'a xpow) sigT

Level-tagged element. At level 0, isomorphic to \'a; at level l > 0, a balanced tree of 2^l base values.

Sourceval to_list : 'a1 t -> 'a1 list

to_list e flattens a level-l element to a list of 2^l base values, in left-to-right order. For a level-0 element built with base x, returns [x].

Sourceval level : 'a1 t -> int

level e is l such that e holds 2^l base values.

Sourceval base : 'a1 -> 'a1 t

base x wraps a base value as a level-0 element. This is the one constructor user code needs.

Sourceval pair : 'a1 t -> 'a1 t -> 'a1 t

Internal: combine two level-l elements into a level-(l+1) element. Used by the cascade machinery.

Sourceval unpair : 'a1 t -> ('a1 t * 'a1 t) option

Internal: dual of pair. Returns None on a level-0 element.