package coq

You can search for identifiers within the package.

in-package search v0.2.0

Formal proof management system

Install

Dune Dependency

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

Authors

T

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

Maintainers

C

coqdev@inria.fr

Sources

coq-8.16.1.tar.gz

sha256=583471c8ed4f227cb374ee8a13a769c46579313d407db67a82d202ee48300e4b

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

Module `AcyclicGraph.Make`Source

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 check_eq : Point.t check_function

Sourceval check_leq : Point.t check_function

Sourceval check_lt : Point.t check_function

Sourceval enforce_eq : Point.t -> Point.t -> t -> t option

Sourceval enforce_leq : Point.t -> Point.t -> t -> t option

Sourceval enforce_lt : Point.t -> Point.t -> t -> t option

Source

val get_explanation : 
  (Point.t * constraint_type * Point.t) ->
  t ->
  (constraint_type * Point.t) list

Assuming that the corresponding call to enforce_* returned None, this will give a trace for the failure.

Sourcetype 'a constraint_fold = (Point.t * constraint_type * Point.t) -> 'a -> 'a

Sourceval constraints_of : t -> 'a constraint_fold -> 'a -> 'a * Point.Set.t list

Sourceval constraints_for : kept:Point.Set.t -> t -> 'a constraint_fold -> 'a -> 'a

Sourceval domain : t -> Point.Set.t

Sourceval choose : (Point.t -> bool) -> t -> Point.t -> Point.t option

High-level representation

Sourcetype node =

| Alias of Point.t
| Node of bool Point.Map.t
(*
Nodes v s.t. u < v (true) or u <= v (false)
*)

Sourcetype repr = node Point.Map.t

Sourceval repr : t -> repr

On This Page

Parameters
Signature
1. High-level representation