(* -------------------------------------------------------------------- *)
open EcUtils
open EcParsetree

open EcCoreGoal.FApi

(* -------------------------------------------------------------------- *)

(* Please, note that WP only operates over assignments and conditional
 * statements.  Any weakening of this restriction may break the
 * soundness of the bounded hoare logic.
 *)

val t_wp :
  ?uselet:bool -> ?cost_pre:EcFol.form ->
  (codepos1 doption) option -> backward

val process_wp : (codepos1 doption) option -> pformula option -> backward