Module Mlw_wp

module Mlw_wp: sig .. end

Weakest preconditions




WP-only builtins


val lemma_label : Ident.label
val fs_at : Term.lsymbol
val fs_old : Term.lsymbol
val t_at_old : Term.term -> Term.term
val mark_theory : Theory.theory
val th_mark_at : Theory.theory
val th_mark_old : Theory.theory
val fs_now : Term.lsymbol
val e_now : Mlw_expr.expr
val remove_old : Term.term -> Term.term
val full_invariant : Decl.known_map ->
Mlw_decl.known_map -> Term.vsymbol -> Mlw_ty.T.ity -> Term.term

Weakest precondition computations


val wp_val : wp:bool ->
Env.env ->
Mlw_decl.known_map ->
Theory.theory_uc -> Mlw_expr.let_sym -> Theory.theory_uc
val wp_let : wp:bool ->
Env.env ->
Mlw_decl.known_map ->
Theory.theory_uc -> Mlw_expr.let_defn -> Theory.theory_uc
val wp_rec : wp:bool ->
Env.env ->
Mlw_decl.known_map ->
Theory.theory_uc -> Mlw_expr.fun_defn list -> Theory.theory_uc