Module Smtml.Binder

Quantifiers and Binding Constructs. This module defines types and utilities for representing quantifiers (universal and existential) and let-bindings, which are commonly used in SMT-LIB formulas for logical quantification and local definitions.

Quantifier and Binding Types

type t =
  1. | Forall
    (*

    Universal quantifier (forall x. P(x)).

    *)
  2. | Exists
    (*

    Existential quantifier (exists x. P(x)).

    *)
  3. | Let_in
    (*

    Let-binding (let x = e in P(x)), used for local definitions.

    *)

A type representing quantifiers and let-bindings in SMT-LIB.

val compare : t -> t -> Ppx_deriving_runtime.int
val equal : t -> t -> bool

equal q1 q2 returns true if the quantifiers or binding constructs q1 and q2 are equal.

val hash : t -> int

An unseeded hash function.

Pretty Printing

val pp : t Fmt.t

Pretty-printer for quantifiers and let-bindings. Formats a value of type t for human-readable output.