package why3

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val is_lsymbol : Term.term -> bool
val create_constant : Ty.ty -> Term.lsymbol * Decl.decl
val return_list : Ty.ty list -> Ty.ty Ty.Mtv.t -> (Term.lsymbol * Decl.decl) list
val my_ls_app_inst : Term.lsymbol -> Ty.ty option -> Ty.ty Ty.Mtv.t
val build_decls : (Term.lsymbol * 'a) list -> Term.term -> Decl.decl list list
val compounds_of : Term.Sls.t -> Term.term -> Term.Sls.t
val destruct_alg : bool -> Term.term -> Task.task Trans.tlist
val instantiate : Decl.prsymbol -> Term.term list -> Task.task Trans.trans
OCaml

Innovation. Community. Security.