package smtml

  1. Overview
  2. Docs
An SMT solver frontend for OCaml

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (26)

Authors

  1. J
    João Pereira <joaomhmpereira@tecnico.ulisboa.pt>
  2. F
    Filipe Marques <filipe.s.marques@tecnico.ulisboa.pt>
  3. H
    Hichem Rami Ait El Hara <hra@ocamlpro.com>
  4. R
    redianthus <redopam@pm.me>
  5. A
    Arthur Carcano <arthur.carcano@ocamlpro.com>
  6. P
    Pierre Chambart <pierre.chambart@ocamlpro.com>
  7. J
    José Fragoso Santos <jose.fragoso@tecnico.ulisboa.pt>

Maintainers

  1. F
    Filipe Marques <filipe.s.marques@tecnico.ulisboa.pt>

Sources

v0.31.0.tar.gz
md5=ba72b873d2220601034a83a5d6b68821
sha512=8d23188fb9e3b228218d38819a162535cc56f370720460ce3ad80db1e8143b6a2631ab2c8e594c52745d4eb0cf2a5d8b205056227fff427f3b76e8dcc719ca0c

doc/src/smtml/binder.ml.html

Source file binder.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
(* SPDX-License-Identifier: MIT *)
(* Copyright (C) 2023-2026 formalsec *)
(* Written by Hichem Rami Ait El Hara *)

(* Dolmen's binders *)
type t =
  | Forall
  | Exists
  | Let_in
[@@deriving ord]

let equal a b =
  match (a, b) with
  | Forall, Forall | Exists, Exists | Let_in, Let_in -> true
  | (Forall | Exists | Let_in), _ -> false

let hash = function Forall -> 0 | Exists -> 1 | Let_in -> 2

let pp fmt = function
  | Forall -> Fmt.string fmt "forall"
  | Exists -> Fmt.string fmt "exists"
  | Let_in -> Fmt.string fmt "let"