package why3

  1. Overview
  2. Docs
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
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
OCaml

Innovation. Community. Security.