package smtml
An SMT solver frontend for OCaml
Install
Dune Dependency
Authors
-
JJoão Pereira <joaomhmpereira@tecnico.ulisboa.pt>
-
FFilipe Marques <filipe.s.marques@tecnico.ulisboa.pt>
-
HHichem Rami Ait El Hara <hra@ocamlpro.com>
-
LLéo Andrès <contact@ndrs.fr>
-
AArthur Carcano <arthur.carcano@ocamlpro.com>
-
PPierre Chambart <pierre.chambart@ocamlpro.com>
-
JJosé Fragoso Santos <jose.fragoso@tecnico.ulisboa.pt>
Maintainers
Sources
v0.8.0.tar.gz
md5=f3384afc4c52ea0fcda2b434892f8412
sha512=47a70d32fae1c833b6a4765ab1152b241e1c60078a30c27b4669bb4a7fe499228d5c5783aca4462ed553408fa16488903924bad11b050bb22a985770796f56af
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(* Dolmen's binders *) type t = | Forall | Exists | Let_in let equal a b = match (a, b) with | Forall, Forall | Exists, Exists | Let_in, Let_in -> true | (Forall | Exists | Let_in), _ -> false let pp fmt = function | Forall -> Fmt.string fmt "forall" | Exists -> Fmt.string fmt "exists" | Let_in -> Fmt.string fmt "let"