package why3

You can search for identifiers within the package.

in-package search v0.2.0

why3
- Why3
  - Abstract_quantifiers
  - Abstraction
  - Alt_ergo
  - Apply
  - Args_wrapper
  - Autodetection
  - BigInt
  - Big_real
  - C
    
    C
    
    MLToC
    
    Print
  - Cakeml
    
    Print
  - Call_provers
  - Case
  - Close_epsilon
  - Cmdline
  - Cntexmp_printer
    
    S
    
    TermCmp
  - Coercion
  - Collect_data_model
  - Compile
    
    InlineFunctionCalls
    
    InlineProxyVars
    
    InlineTrivialLets
    
    RefreshLetBindings
    
    Transform
    
    Translate
  - Compress
    
    Compress_none
    
    Compress_z
    
    S
  - Compute
  - Config
  - Congruence
  - Constant
  - Controller_itp
    
    Make
    
    _
    
    Scheduler
  - Coq
  - Cut
  - Cvc3
  - Debug
    
    Args
    
    Stats
  - Decl
    
    DeclTF
    
    Hdecl
    
    Hpr
    
    Mdecl
    
    Mpr
    
    Sdecl
    
    M
    
    Spr
    
    M
    
    Wdecl
    
    Wpr
  - Destruct
  - Detect_polymorphism
  - Dexpr
  - Diffmap
    
    Make
    
    M
    
    MakeOfMap
    
    M
    
    S
    
    M
  - Discriminate
    
    Lsmap
  - Driver
  - Driver_ast
  - Driver_lexer
  - Driver_parser
    
    Incremental
    
    MenhirInterpreter
  - Dterm
  - Eliminate_algebraic
  - Eliminate_definition
  - Eliminate_epsilon
  - Eliminate_if
  - Eliminate_inductive
  - Eliminate_let
  - Eliminate_literal
  - Eliminate_symbol
  - Eliminate_unknown_lsymbols
  - Eliminate_unknown_types
  - Encoding
  - Encoding_guards
  - Encoding_guards_full
  - Encoding_select
    
    Kept
    
    Lsinst
    
    Lskept
  - Encoding_sort
  - Encoding_tags
  - Encoding_tags_full
  - Encoding_twin
  - Env
    
    Wenv
  - Eval_match
  - Exn_printer
  - Expr
    
    Hrs
    
    Mrs
    
    Srs
    
    M
    
    Wrs
  - Exthtbl
    
    Make
    
    Private
    
    S
  - Extmap
    
    Make
    
    S
  - Extset
    
    Make
    
    M
    
    MakeOfMap
    
    M
    
    S
    
    M
  - Filter_trigger
  - Gappa
  - Generic_arg_trans_utils
  - Glob
  - Hashcons
    
    HashedType
    
    Make
    
    H
    
    S
  - Ident
    
    Hid
    
    Mattr
    
    Mid
    
    Sattr
    
    M
    
    Sid
    
    M
    
    Wid
  - Ind_itp
  - Induction
  - Induction_pr
  - Inlining
  - Instantiate_predicate
  - Intro_projections_counterexmp
  - Intro_vc_vars_counterexmp
  - Introduction
  - Isabelle
  - Itp_communication
  - Itp_server
    
    Make
    
    _
    
    Protocol
  - Ity
    
    Hits
    
    Hity
    
    Hpv
    
    Hreg
    
    Mits
    
    Mity
    
    Mpv
    
    Mreg
    
    Mxs
    
    Sits
    
    M
    
    Sity
    
    M
    
    Spv
    
    M
    
    Sreg
    
    M
    
    Sxs
    
    M
    
    Wits
    
    Wity
    
    Wpv
    
    Wreg
  - Json_base
  - Json_lexer
  - Json_parser
    
    Incremental
    
    MenhirInterpreter
  - Json_util
  - Lexer
  - Lexlib
  - Libencoding
  - Lift_epsilon
  - Lists
  - Loc
  - Matching
    
    C
    
    Cpat
    
    Cty
    
    IL
    
    Instr
    
    MC
    
    MCpat
    
    MCty
    
    MIL
    
    MInstr
    
    TyG
  - Mathematica
  - Ml_printer
    
    MLPrinter
    
    _
    
    S
  - Mlinterp
  - Mlmpfr_wrapper
  - Mltree
  - Mlw_printer
  - Model_parser
  - Number
  - Ocaml
    
    Print
  - Opt
  - Parse_smtv2_model
  - Parse_smtv2_model_lexer
  - Parse_smtv2_model_parser
    
    Incremental
    
    MenhirInterpreter
  - Parser
    
    Incremental
    
    MenhirInterpreter
  - Parser_messages
  - Pattern
  - Pdecl
  - Pdriver
  - Pinterp
  - Plugin
  - Pmodule
  - Pp
    
    Ansi
  - Pqueue
    
    Make
    
    X
  - Prepare_for_counterexmp
  - Pretty
    
    Printer
  - Print_tree
    
    Make
    
    T
    
    PMake
    
    T
    
    PTree
    
    Tree
  - Printer
  - Prop_curry
  - Prove_client
  - Ptree
  - Pvs
  - Rc
  - Re
  - Reduction_engine
  - Reflection
  - Report
  - Server_utils
  - Session_itp
    
    Hfile
    
    Hpan
    
    Hpn
    
    Htn
  - Simplify
  - Simplify_array
  - Simplify_formula
  - Smoke_detector
  - Smt2_model_defs
  - Smtv1
  - Smtv2
  - Split_goal
  - Strategy
  - Strategy_parser
  - Strings
  - Subst
  - Sysutil
  - Task
  - Term
    
    Hls
    
    Hterm
    
    Hterm_strict
    
    Hvs
    
    Mls
    
    Mterm
    
    Mterm_strict
    
    Mvs
    
    Sls
    
    M
    
    Sterm
    
    M
    
    Sterm_strict
    
    M
    
    Svs
    
    M
    
    TermTF
    
    Wls
    
    Wvs
  - Termcode
    
    Gshape
    
    Pairing
    
    New
    
    Old
    
    S
  - Theory
    
    Hmeta
    
    Htdecl
    
    Mmeta
    
    Mtdecl
    
    Smeta
    
    M
    
    Stdecl
    
    M
  - Trans
  - Ty
    
    Hts
    
    Htv
    
    Hty
    
    Mts
    
    Mtv
    
    Mty
    
    Sts
    
    M
    
    Stv
    
    M
    
    Sty
    
    M
    
    Wts
    
    Wty
  - Typeinv
  - Typing
  - Unix_scheduler
    
    Unix_scheduler
  - Util
  - Vc
  - Vector
  - Warning
  - Weakhtbl
    
    Make
    
    S
    
    S
    
    Weakey
  - Why3printer
  - Whyconf
    
    Args
    
    Hprover
    
    Meditor
    
    Mprover
    
    Prover
    
    Sprover
    
    M
  - Wstdlib
    
    Hfloat
    
    Hint
    
    Hstr
    
    Int
    
    MakeMSH
    
    H
    
    M
    
    S
    
    M
    
    X
    
    MakeMSHW
    
    H
    
    M
    
    S
    
    M
    
    W
    
    X
    
    Mfloat
    
    Mint
    
    Mstr
    
    OrderedHashed
    
    X
    
    OrderedHashedList
    
    X
    
    OrderedHashedType
    
    Sfloat
    
    M
    
    Sint
    
    M
    
    Sstr
    
    M
    
    TaggedType
  - Xml
  - Yices

Legend:
Library
Module
Module type
Parameter
Class
Class type

val coercion_attr : Ident.attribute

val why3_keywords : string list

val prio_binop : Term.binop -> int

val protect_on : 
  bool ->
  ('a, 'b, 'c, 'd, 'e, 'f) Stdlib.format6 ->
  ('a, 'b, 'c, 'd, 'e, 'f) Stdlib.format6

type syntax =

| Is_array of string
| Is_getter of string
| Is_none

val get_element_syntax : attrs:Ident.Sattr.t -> syntax

module type Printer = sig ... end

val tprinter : Ident.ident_printer

val aprinter : Ident.ident_printer

val sprinter : Ident.ident_printer

val pprinter : Ident.ident_printer

val forget_all : unit -> unit

val forget_tvs : unit -> unit

val forget_var : Term.vsymbol -> unit

val print_id_attrs : Stdlib.Format.formatter -> Ident.ident -> unit

val print_tv : Stdlib.Format.formatter -> Ty.tvsymbol -> unit

val print_vs : Stdlib.Format.formatter -> Term.vsymbol -> unit

val print_ts : Stdlib.Format.formatter -> Ty.tysymbol -> unit

val print_ls : Stdlib.Format.formatter -> Term.lsymbol -> unit

val print_cs : Stdlib.Format.formatter -> Term.lsymbol -> unit

val print_pr : Stdlib.Format.formatter -> Decl.prsymbol -> unit

val print_th : Stdlib.Format.formatter -> Theory.theory -> unit

val print_ty : Stdlib.Format.formatter -> Ty.ty -> unit

val print_vsty : Stdlib.Format.formatter -> Term.vsymbol -> unit

val print_ts_qualified : Stdlib.Format.formatter -> Ty.tysymbol -> unit

val print_ls_qualified : Stdlib.Format.formatter -> Term.lsymbol -> unit

val print_cs_qualified : Stdlib.Format.formatter -> Term.lsymbol -> unit

val print_pr_qualified : Stdlib.Format.formatter -> Decl.prsymbol -> unit

val print_th_qualified : Stdlib.Format.formatter -> Theory.theory -> unit

val print_ty_qualified : Stdlib.Format.formatter -> Ty.ty -> unit

val print_quant : Stdlib.Format.formatter -> Term.quant -> unit

val print_binop : asym:bool -> Stdlib.Format.formatter -> Term.binop -> unit

val print_pat : Stdlib.Format.formatter -> Term.pattern -> unit

val print_term : Stdlib.Format.formatter -> Term.term -> unit

val print_attr : Stdlib.Format.formatter -> Ident.attribute -> unit

val print_loc : Stdlib.Format.formatter -> Loc.position -> unit

val print_pkind : Stdlib.Format.formatter -> Decl.prop_kind -> unit

val print_meta_arg : Stdlib.Format.formatter -> Theory.meta_arg -> unit

val print_meta_arg_type : 
  Stdlib.Format.formatter ->
  Theory.meta_arg_type ->
  unit

val print_ty_decl : Stdlib.Format.formatter -> Ty.tysymbol -> unit

val print_data_decl : Stdlib.Format.formatter -> Decl.data_decl -> unit

val print_param_decl : Stdlib.Format.formatter -> Term.lsymbol -> unit

val print_logic_decl : Stdlib.Format.formatter -> Decl.logic_decl -> unit

val print_ind_decl : 
  Stdlib.Format.formatter ->
  Decl.ind_sign ->
  Decl.ind_decl ->
  unit

val print_next_data_decl : Stdlib.Format.formatter -> Decl.data_decl -> unit

val print_next_logic_decl : Stdlib.Format.formatter -> Decl.logic_decl -> unit

val print_next_ind_decl : Stdlib.Format.formatter -> Decl.ind_decl -> unit

val print_prop_decl : Stdlib.Format.formatter -> Decl.prop_decl -> unit

val print_decl : Stdlib.Format.formatter -> Decl.decl -> unit

val print_tdecl : Stdlib.Format.formatter -> Theory.tdecl -> unit

val print_task : Stdlib.Format.formatter -> Task.task -> unit

val print_sequent : Stdlib.Format.formatter -> Task.task -> unit

val print_theory : Stdlib.Format.formatter -> Theory.theory -> unit

val print_namespace : 
  Stdlib.Format.formatter ->
  string ->
  Theory.theory ->
  unit

type any_pp =

| Pp_term of Term.term * int
| Pp_ty of Ty.ty * int * bool
| Pp_decl of bool * Ty.tysymbol * (Term.lsymbol * Term.lsymbol option list) list
| Pp_ts of Ty.tysymbol
| Pp_ls of Term.lsymbol
| Pp_id of Ident.ident
| Pp_cs of Term.lsymbol
| Pp_vs of Term.vsymbol
| Pp_trigger of Term.trigger
| Pp_forget of Term.vsymbol list
| Pp_forget_tvs

val create : 
  ?print_ext_any:(any_pp Pp.pp -> any_pp Pp.pp) ->
  Ident.ident_printer ->
  Ident.ident_printer ->
  Ident.ident_printer ->
  Ident.ident_printer ->
  bool ->
  (module Printer)