package colibri2

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

A scope for decision, allows to wait before adding decisions for terms. Used for propagating into a term without decisions

val create : _ Egraph.t -> t

Create a new group

val activate : _ Egraph.t -> t -> unit
val add_to_group : _ Egraph.t -> ThTerm.t -> t -> unit

Add a ThTerm.t to a group

val make_choosable : _ Egraph.t -> ThTerm.t -> unit

Register the decisions attached to the node, and will not delay them in the future

val add_to_group_of : _ Egraph.t -> ThTerm.t -> ThTerm.t -> unit

add_to_group_of d t1 t2 add t1 in the group of t2

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