package coq

  1. Overview
  2. Docs
Formal proof management system

Install 

dune-project
 Dependency

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

Authors

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

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.16.1.tar.gz
sha256=583471c8ed4f227cb374ee8a13a769c46579313d407db67a82d202ee48300e4b

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.