package why3

  1. Overview
  2. Docs
package why3
Legend:
Library
Module
Module type
Parameter
Class
Class type
type fformat = string
type filename = string
type extension = string
type pathname = string list
type env
val env_tag : env -> Weakhtbl.tag
module Wenv : sig ... end
val create_env : filename list -> env
val get_loadpath : env -> filename list
type 'a language
val register_language : 'a language -> ('b -> 'a) -> 'b language
val add_builtin : 'a language -> (pathname -> 'a) -> unit
val base_language_builtin : pathname -> Theory.theory Wstdlib.Mstr.t
type !'a format_parser = env -> pathname -> filename -> in_channel -> 'a
exception KnownFormat of fformat
val register_format : desc:Pp.formatted -> 'a language -> fformat -> extension list -> 'a format_parser -> unit
val list_formats : 'a language -> (fformat * extension list * Pp.formatted) list
exception InvalidFormat of fformat
exception UnknownFormat of fformat
exception UnknownExtension of extension
exception UnspecifiedFormat
val read_channel : ?format:fformat -> 'a language -> env -> filename -> in_channel -> 'a
val read_file : ?format:fformat -> 'a language -> env -> filename -> 'a
exception LibraryNotFound of pathname
exception LibraryConflict of pathname
exception AmbiguousPath of filename * filename
val read_library : 'a language -> env -> pathname -> 'a
val locate_library : env -> pathname -> filename
exception TheoryNotFound of pathname * string
val read_theory : env -> pathname -> string -> Theory.theory
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