package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

Parameters

module Point : Point

Signature

type t
val empty : t
val check_invariants : required_canonical:(Point.t -> bool) -> t -> unit
exception AlreadyDeclared
val add : ?rank:int -> Point.t -> t -> t
exception Undeclared of Point.t
val check_declared : t -> Point.Set.t -> unit
type !'a check_function = t -> 'a -> 'a -> bool
val check_eq : Point.t check_function
val check_leq : Point.t check_function
val check_lt : Point.t check_function
val enforce_eq : Point.t -> Point.t -> t -> t
val enforce_leq : Point.t -> Point.t -> t -> t
val enforce_lt : Point.t -> Point.t -> t -> t
val constraints_of : t -> Point.Constraint.t * Point.Set.t list
val constraints_for : kept:Point.Set.t -> t -> Point.Constraint.t
val domain : t -> Point.Set.t
val choose : (Point.t -> bool) -> t -> Point.t -> Point.t option
val sort : (int -> Point.t) -> Point.t list -> t -> t
val pr : (Point.t -> Pp.t) -> t -> Pp.t
val dump : (constraint_type -> Point.t -> Point.t -> unit) -> t -> unit