package why3

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

val debug : Debug.flag

val meta_kept : Theory.meta

val meta_base : Theory.meta

val ts_type : Ty.tysymbol

val ty_type : Ty.ty

val d_ts_type : Decl.decl

val ls_of_ts : Ty.tysymbol -> Term.lsymbol

val term_of_ty : Term.term Ty.Mtv.t -> Ty.ty -> Term.term

val ls_extend : Term.lsymbol -> Term.lsymbol

val type_close : 
  Ty.Stv.t ->
  (Term.term Ty.Mtv.t -> 'a -> Term.term) ->
  'a ->
  Term.term

val t_type_close : 
  (Term.term Ty.Mtv.t -> Term.term -> Term.term) ->
  Term.term ->
  Term.term

val lsdecl_of_ts : Ty.tysymbol -> Decl.decl

val id_unprotected : string -> Ident.preid

val is_protected_id : Ident.ident -> bool

val id_unprotecting : string -> Ident.preid

val is_protecting_id : Ident.ident -> bool

val is_protected_vs : Ty.Sty.t -> Term.vsymbol -> bool

val is_protected_ls : Ty.Sty.t -> Term.lsymbol -> bool

val d_monomorph : 
  Ty.ty ->
  Ty.Sty.t ->
  (Term.lsymbol -> Term.lsymbol) ->
  Decl.decl ->
  Decl.decl list

val monomorphise_task : Task.task Trans.trans

val monomorphise_goal : Task.task Trans.trans

val close_kept : Task.task Trans.trans

val defn_or_axiom : Term.lsymbol -> Term.term -> Decl.decl list