package why3

  1. Overview
  2. Docs
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 = {
  1. rem_pr : Decl.Spr.t;
  2. rem_ls : Term.Sls.t;
  3. rem_ts : Ty.Sts.t;
  4. rem_nt : Trans.naming_table;
}
type bisect_step =
  1. | BSdone of rem
  2. | BSstep of rem * bool -> bisect_step
val bisect_step : Task.task -> bisect_step
OCaml

Innovation. Community. Security.