package coq-core

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

Install 

dune-project
 Dependency

coq.inria.fr Edit opam file Versions (11)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.19.0.tar.gz
md5=64b49dbc3205477bd7517642c0b9cbb6
sha512=02fb5b4fb575af79e092492cbec6dc0d15a1d74a07f827f657a72d4e6066532630e5a6d15be4acdb73314bd40b9a321f9ea0584e0ccfe51fd3a56353bd30db9b

doc/coq-core.clib/IStream/index.html

Module IStreamSource

Purely functional streams

Contrarily to OCaml module Stream, these are meant to be used purely functionally. This implies in particular that accessing an element does not discard it.

Sourcetype +'a t

Type of pure streams.

Sourcetype 'a node =
  1. | Nil
  2. | Cons of 'a * 'a t
    (*

    View type to decompose and build streams.

    *)
Constructors
Sourceval empty : 'a t

The empty stream.

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

Append an element in front of a stream.

Sourceval thunk : (unit -> 'a node) -> 'a t

Internalize the laziness of a stream.

Destructors
Sourceval is_empty : 'a t -> bool

Whethere a stream is empty.

Sourceval peek : 'a t -> 'a node

Return the head and the tail of a stream, if any.

Standard operations

All stream-returning functions are lazy. The other ones are eager.

Sourceval app : 'a t -> 'a t -> 'a t

Append two streams. Not tail-rec.

Sourceval map : ('a -> 'b) -> 'a t -> 'b t

Mapping of streams. Not tail-rec.

Sourceval iter : ('a -> unit) -> 'a t -> unit

Iteration over streams.

Sourceval fold : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a

Fold over streams.

Sourceval concat : 'a t t -> 'a t

Appends recursively a stream of streams.

Sourceval map_filter : ('a -> 'b option) -> 'a t -> 'b t

Mixing map and filter. Not tail-rec.

Sourceval concat_map : ('a -> 'b t) -> 'a t -> 'b t

concat_map f l is the same as concat (map f l).

Conversions
Sourceval of_list : 'a list -> 'a t

Convert a list into a stream.

Sourceval to_list : 'a t -> 'a list

Convert a stream into a list.

Other
Sourceval force : 'a t -> 'a t

Forces the whole stream.