package why3find

You can search for identifiers within the package.

in-package search v0.2.0

Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module `Why3find.Wutil`Source

Sourceval exts : unit -> string list

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

Sourceval filepath : string -> string * string list

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

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

Iterates over declared id.

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

Iterates over declared id.

Sourceval 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).

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

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

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

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

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

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

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