package smtml

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

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 equal : t -> t -> bool

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

Pretty Printing

val pp : t Fmt.t

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

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