package why3find

You can search for identifiers within the package.

in-package search v0.2.0

Legend:
Library
Module
Module type
Parameter
Class
Class type

val exts : unit -> string list

All recognized extensions. Typically ".mlw" and other from plugins.

val filepath : string -> string * string list

val load_theories : 
  Why3.Env.env ->
  Why3.Env.filename ->
  Why3.Theory.theory list * Why3.Env.fformat

val iter_decl : (Why3.Ident.ident -> unit) -> Why3.Decl.decl -> unit

Iterates over declared id.

val iter_tdecl : (Why3.Ident.ident -> unit) -> Why3.Theory.tdecl -> unit

Iterates over declared id.

val iter_pdecl : (Why3.Ident.ident -> unit) -> Why3.Pdecl.pdecl -> unit

Iterates over declared id.

val iter_sm : 
  (Why3.Ident.ident -> Why3.Ident.ident -> unit) ->
  Why3.Theory.symbol_map ->
  unit

Iterates over mapped identifiers (source, target).

val iter_mi : 
  (Why3.Ident.ident -> Why3.Ident.ident -> unit) ->
  Why3.Pmodule.mod_inst ->
  unit

Iterates over mapped identifiers (source, target).

val pp_thy : Format.formatter -> Why3.Theory.theory -> unit

val pp_mod : Format.formatter -> Why3.Pmodule.pmodule -> unit

val pp_pdecl : Format.formatter -> Why3.Pdecl.pdecl -> unit

val pp_tdecl : Format.formatter -> Why3.Theory.tdecl -> unit

val pp_munit : Format.formatter -> Why3.Pmodule.mod_unit -> unit

val pp_theory : Format.formatter -> Why3.Theory.theory -> unit

val pp_module : Format.formatter -> Why3.Pmodule.pmodule -> unit