package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
type 'a forest = 'a tree list

The intent is that an 'a forest is a list of messages of type 'a. But messages can stand for a list of more precise messages, hence the structure is organised as a tree.

and 'a tree =
  1. | Seq of 'a * 'a forest
type 'a incr

To build a trace incrementally, we use an intermediary data structure on which we can define an S-expression like language (like a simplified xml except the closing tags do not carry a name).

val to_tree : 'a incr -> 'a forest
val opn : 'a -> 'a incr -> 'a incr

open a opens a tag with name a.

val close : 'a incr -> 'a incr

close closes the last open tag. It is the responsibility of the user to close all the tags.

val leaf : 'a -> 'a incr -> 'a incr

leaf creates an empty tag with name a.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct