package why3

You can search for identifiers within the package.

in-package search v0.2.0

package why3

why3
- Why3
  - Abstract_quantifiers
  - Abstraction
  - Alt_ergo
  - Apply
  - Args_wrapper
  - Autodetection
  - BigInt
  - Cakeml_printer
    
    Print
  - Call_provers
  - Case
  - Close_epsilon
  - Cmdline
  - Cntexmp_printer
    
    S
    
    TermCmp
  - Coercion
  - Collect_data_model
  - Compile
    
    Transform
    
    Translate
  - Compress
    
    Compress_none
    
    Compress_z
    
    S
  - Compute
  - Config
  - Controller_itp
    
    Make
    
    S
    
    Scheduler
  - Coq
  - Cprinter
    
    C
    
    MLToC
    
    Print
  - Cut
  - Cvc3
  - Debug
    
    Args
    
    Stats
  - Decl
    
    DeclTF
    
    Hdecl
    
    Hpr
    
    Mdecl
    
    Mpr
    
    Sdecl
    
    M
    
    Spr
    
    M
    
    Wdecl
    
    Wpr
  - Destruct
  - Detect_polymorphism
  - Dexpr
  - 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
    
    P
    
    S
    
    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
    
    K
    
    S
  - Mlinterp
  - Mltree
  - Model_parser
  - Number
  - Ocaml_printer
    
    Print
  - Opt
  - Parse_smtv2_model
  - Parse_smtv2_model_lexer
  - Parse_smtv2_model_parser
    
    Incremental
    
    MenhirInterpreter
  - Parser
    
    Incremental
    
    MenhirInterpreter
  - 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
  - Reduction_engine
  - Reflection
  - Server_utils
  - Session_itp
    
    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_nt_na
    
    Hvs
    
    Mls
    
    Mterm
    
    Mvs
    
    Sls
    
    M
    
    Sterm
    
    M
    
    Svs
    
    M
    
    TermTF
    
    Wls
    
    Wvs
  - Termcode
    
    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
  - Util
  - Vc
  - Vector
  - Warning
  - Weakhtbl
    
    Make
    
    S
    
    S
    
    Weakey
  - Why3printer
  - Whyconf
    
    Args
    
    Hprover
    
    Meditor
    
    Mprover
    
    Prover
    
    Sprover
    
    M
  - Wstdlib
    
    Hfloat
    
    Hint
    
    Hstr
    
    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
why3.extract
- Why3extract

Legend:
Library
Module
Module type
Parameter
Class
Class type

exception Arg_trans of string

exception Arg_trans_decl of string * Theory.tdecl list

exception Arg_trans_term of string * Term.term

exception Arg_trans_term2 of string * Term.term * Term.term

exception Arg_trans_pattern of string * Term.pattern * Term.pattern

exception Arg_trans_type of string * Ty.ty * Ty.ty

exception Arg_trans_missing of string * Term.Svs.t

exception Arg_bad_hypothesis of string * Term.term

exception Cannot_infer_type of string

exception Unnecessary_terms of Term.term list

val gen_ident : 
  ?attrs:Ident.Sattr.t ->
  ?loc:Loc.position ->
  string ->
  Ident.preid

val replace_in_term : Term.term -> Term.term -> Term.term -> Term.term

val subst_quant : Term.quant -> Term.term_quant -> Term.term -> Term.term

val subst_exist : Term.term -> Term.term -> Term.term

val subst_forall : Term.term -> Term.term -> Term.term

val subst_forall_list : Term.term -> Term.term list -> Term.term

val get_local : Decl.decl list Trans.trans

val get_local_task : Task.task -> Decl.decl list

val sort : Task.task Trans.trans

type term_subst = Term.term Term.Mterm.t

val replace_subst : term_subst -> Term.term -> Term.term

val replace_decl : term_subst -> Decl.decl -> Decl.decl

val replace_tdecl : term_subst -> Theory.tdecl -> Theory.tdecl

val create_goal : expl:string -> Decl.prsymbol -> Term.term -> Decl.decl