package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install

Dune Dependency

Authors

Maintainers

Sources

coq-8.19.1.tar.gz
md5=13d2793fc6413aac5168822313e4864e
sha512=ec8379df34ba6e72bcf0218c66fef248b0e4c5c436fb3f2d7dd83a2c5f349dd0874a67484fcf9c0df3e5d5937d7ae2b2a79274725595b4b0065a381f70769b42

doc/coq-core.gramlib/Gramlib/Stream/index.html

Module Gramlib.StreamSource

Streams and parsers.

Sourcetype ('e, 'a) t

The type of streams holding values of type 'a. Producing a new value needs an environment 'e.

Sourceexception Failure

Raised by streams when trying to access beyond their end.

Stream builders

Sourceval from : ?offset:int -> ('e -> 'a option) -> ('e, 'a) t

Stream.from f returns a stream built from the function f. To create a new stream element, the function f is called. The user function f must return either Some <value> for a value or None to specify the end of the stream. offset will initialize the stream count to start with offset consumed items, which is useful for some uses cases such as parsing resumption.

Sourceval empty : unit -> ('e, 'a) t

Return the stream holding the elements of the list in the same order.

Sourceval of_string : ?offset:int -> string -> (unit, char) t

Return the stream of the characters of the string parameter. If set. offset parameter is similar to from.

Sourceval of_channel : in_channel -> (unit, char) t

Return the stream of the characters read from the input channel.

Predefined parsers

Sourceval next : 'e -> ('e, 'a) t -> 'a

Return the first element of the stream and remove it from the stream.

Sourceval is_empty : 'e -> ('e, 'a) t -> bool

Return true if the stream is empty, else false.

Useful functions

Sourceval peek : 'e -> ('e, 'a) t -> 'a option

Return Some of "the first element" of the stream, or None if the stream is empty.

Sourceval junk : 'e -> ('e, 'a) t -> unit

Remove the first element of the stream, possibly unfreezing it before.

Sourceval count : ('e, 'a) t -> int

Return the current count of the stream elements, i.e. the number of the stream elements discarded.

Sourceval npeek : 'e -> int -> ('e, 'a) t -> 'a list

npeek e n returns the list of the n first elements of the stream, or all its remaining elements if less than n elements are available.

Sourceval nth : 'e -> int -> ('e, 'a) t -> 'a
Sourceval njunk : 'e -> int -> ('e, 'a) t -> unit
OCaml

Innovation. Community. Security.