Module Vc

module Vc: sig .. end

WhyML VC generators

val sp_attr : Ident.attribute

val wp_attr : Ident.attribute

val kp_attr : Ident.attribute

val wb_attr : Ident.attribute

val nt_attr : Ident.attribute

val set_infer_invs : (Ident.Sattr.t ->
        Env.env ->
        Decl.known_map ->
        Pdecl.known_map -> Expr.expr -> Ity.cty -> (Expr.expr * Term.term) list) ->
       unit

val warn_missing_diverges : Loc.warning_id

val vc : Env.env ->
       Pdecl.known_map -> Theory.theory_uc -> Pdecl.pdecl -> Pdecl.pdecl list