package why3

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type driver
val load_driver_absolute : Env.env -> string -> string list -> driver
val file_of_task : driver -> string -> string -> Task.task -> string
val file_of_theory : driver -> string -> Theory.theory -> string
val print_task : ?old:in_channel -> driver -> Format.formatter -> Task.task -> unit
val print_theory : ?old:in_channel -> driver -> Format.formatter -> Theory.theory -> unit
val prove_task : command:string -> limit:Call_provers.resource_limit -> ?old:string -> ?inplace:bool -> ?interactive:bool -> driver -> Task.task -> Call_provers.prover_call
val prepare_task : driver -> Task.task -> Task.task
val print_task_prepared : ?old:in_channel -> driver -> Format.formatter -> Task.task -> Printer.printer_mapping
val prove_task_prepared : command:string -> limit:Call_provers.resource_limit -> ?old:string -> ?inplace:bool -> ?interactive:bool -> driver -> Task.task -> Call_provers.prover_call
val syntax_map : driver -> Printer.syntax_map
OCaml

Innovation. Community. Security.