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
    
    Ord
    
    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
    
    X
    
    Private
    
    S
  - Extmap
    
    Make
    
    Ord
    
    S
  - Extset
    
    Make
    
    M
    
    Ord
    
    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 eliminate_builtin : Task.task Trans.trans

val compute_diff : 
  (Theory.meta * Theory.meta_arg list) list Trans.trans Trans.trans

val eliminate_definition_func : Task.task Trans.trans

val eliminate_definition_pred : Task.task Trans.trans

val eliminate_definition : Task.task Trans.trans

val eliminate_definition_gen : (Term.lsymbol -> bool) -> Task.task Trans.trans

val eliminate_mutual_recursion : Task.task Trans.trans

type rem = {

rem_pr : Decl.Spr.t;
rem_ls : Term.Sls.t;
rem_ts : Ty.Sts.t;
rem_nt : Trans.naming_table;

}

type bisect_step =

| BSdone of rem
| BSstep of rem * bool -> bisect_step

val bisect_step : Task.task -> bisect_step