package rocq-runtime

  1. Overview
  2. Docs

Module SListSource

Sparse lists.

Constructors
Sourcetype +'a t = private
  1. | Nil
  2. | Cons of 'a * 'a t
  3. | Default of int * 'a t
    (*

    'a t is an efficient representation of 'a option list.

    *)
Sourceval empty : 'a t

The empty list.

Sourceval cons : 'a -> 'a t -> 'a t

Isomorphic to Some x :: l.

Sourceval default : 'a t -> 'a t

Isomorphic to None :: l.

Sourceval cons_opt : 'a option -> 'a t -> 'a t

cons if Some, default otherwise

Sourceval defaultn : int -> 'a t -> 'a t

Iterated variant of default.

Destructor
Sourceval view : 'a t -> ('a option * 'a t) option
Sourceval is_empty : 'a t -> bool
Sourceval is_default : 'a t -> bool
Usual list-like operators
Sourceval length : 'a t -> int
Sourceval equal : ('a -> 'b -> bool) -> 'a t -> 'b t -> bool
Sourceval compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
Sourceval to_list : 'a t -> 'a option list
Sourceval of_full_list : 'a list -> 'a t
Iterators ignoring optional values
Sourcemodule Skip : sig ... end

These iterators ignore the default values in the list.

Smart iterators
Sourcemodule Smart : sig ... end

These iterators also ignore the default values in the list.