package why3

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val debug_matching : Debug.flag
val intros : Term.term -> Term.term list * Term.vsymbol list * Term.term
val term_decl : Theory.tdecl -> Term.term
val with_terms : trans_name:string -> Ty.ty Ty.Mtv.t -> Term.term Term.Mvs.t -> Term.Mvs.key list -> Term.term list -> Ty.ty Ty.Mtv.t * Term.term Term.Mvs.t
val matching_with_terms : trans_name:string -> Term.Svs.t -> Term.Mvs.key list -> Term.term -> Term.term -> Term.term list option -> Ty.ty Ty.Mtv.t * Term.term Term.Mvs.t
val apply : Decl.prsymbol -> Term.term list option -> Task.task Trans.tlist
val replace_subst : Term.term list -> Term.Mvs.key list -> Term.term -> Term.term -> Term.term list -> Term.term -> Term.term list * Term.term
val rewrite_in : bool -> Term.term list -> Decl.prsymbol -> Decl.prsymbol -> Task.task list Trans.trans
val find_target_prop : Decl.prsymbol option -> Decl.prsymbol Trans.trans
val rewrite : Term.term list option -> bool -> Decl.prsymbol -> Decl.prsymbol option -> Task.task list Trans.trans
val rewrite_list : Term.term list option -> bool -> bool -> Decl.prsymbol list -> Decl.prsymbol option -> Task.task list Trans.trans
val detect_prop : Decl.prsymbol -> Decl.prop_kind -> Decl.prsymbol option -> bool
val detect_prop_list : Decl.prsymbol -> Decl.prop_kind -> Decl.prsymbol list option -> bool
val replace : Term.term -> Term.term -> Decl.prsymbol list option -> Task.task Trans.tlist
val t_replace_app : Term.lsymbol -> (Term.Mvs.key list * Term.term) -> Term.term -> Term.term
val t_ls_replace : Term.lsymbol -> (Term.Mvs.key list * Term.term) -> Term.term -> Term.term
val unfold : Term.lsymbol -> Decl.prsymbol list option -> Task.task Trans.trans
OCaml

Innovation. Community. Security.