package why3

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

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_term3 of string * Term.term * 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

exception Remove_unknown of Decl.decl * Ident.ident

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

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