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.15.2.tar.gz
sha256=13a67c0a4559ae22e9765c8fdb88957b16c2b335a2d5f47e4d6d9b4b8b299926

doc/coq-core.lib/AcyclicGraph/Make/index.html

Module AcyclicGraph.MakeSource

Parameters

module Point : Point

Signature

Sourcetype t
Sourceval empty : t
Sourceval check_invariants : required_canonical:(Point.t -> bool) -> t -> unit
Sourceexception AlreadyDeclared
Sourceval add : ?rank:int -> Point.t -> t -> t

All points must be pre-declared through this function before they can be mentioned in the others. NB: use a large rank to keep the node canonical

Sourceexception Undeclared of Point.t
Sourceval check_declared : t -> Point.Set.t -> unit
  • raises Undeclared

    if one of the points is not present in the graph.

Sourcetype 'a check_function = t -> 'a -> 'a -> bool
Sourceval enforce_eq : Point.t -> Point.t -> t -> t
Sourceval enforce_leq : Point.t -> Point.t -> t -> t
Sourceval enforce_lt : Point.t -> Point.t -> t -> t
Sourceval constraints_of : t -> Point.Constraints.t * Point.Set.t list
Sourceval constraints_for : kept:Point.Set.t -> t -> Point.Constraints.t
Sourceval domain : t -> Point.Set.t
Sourceval choose : (Point.t -> bool) -> t -> Point.t -> Point.t option
High-level representation
Sourcetype node =
  1. | Alias of Point.t
  2. | Node of bool Point.Map.t
    (*

    Nodes v s.t. u < v (true) or u <= v (false)

    *)
Sourceval repr : t -> repr