Module QedSource

Sourcemodule Bvars : sig ... end

Bound Variables Footprints.

Sourcemodule Cache : sig ... end
Sourcemodule Collection : sig ... end

Merging Maps and Sets

Sourcemodule Engine : sig ... end

Generic Engine Signature

Sourcemodule Export : sig ... end

Export Engine Factory

Sourcemodule Export_why3 : sig ... end

Exportation Engine for Why-3.

Sourcemodule Export_whycore : sig ... end

Common Exportation Engine for Why-3 and Alt-Ergo

Sourcemodule Hcons : sig ... end

Hash-Consing Utilities

Sourcemodule Idxmap : sig ... end

Map with indexed keys

Sourcemodule Idxset : sig ... end

Set of indexed elements implemented as Patricia sets.

Sourcemodule Intmap : sig ... end

Maps with integers keys using Patricia Trees.

Sourcemodule Intset : sig ... end

Set of integers using Patricia Trees.

Sourcemodule Kind : sig ... end

Logic Types Utilities

Sourcemodule Listmap : sig ... end

Merging List-Association Functor

Sourcemodule Listset : sig ... end

Merging Set Functor

Sourcemodule Logic : sig ... end
Sourcemodule Mergemap : sig ... end

Merging Map Functor

Sourcemodule Mergeset : sig ... end

Merging Set Functor

Sourcemodule Partition : sig ... end

Union-find based partitions

Sourcemodule Plib : sig ... end

Pretty Printing Utilities.

Sourcemodule Pool : sig ... end
Sourcemodule Pretty : sig ... end

Pretty Printer for Qed Output.

Sourcemodule Term : sig ... end

Logic expressions