package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

Module type `Diff2.SeqType`Source

Input signature of Diff.Make.

Sourcetype t

The type of the sequence.

Sourcetype elem

The type of the elements of the sequence.

Sourceval get : t -> int -> elem

get t n returns n-th element of the sequence t.

Sourceval length : t -> int

length t returns the length of the sequence t.