pub fn wp_ty() -> Expr
WP: weakest precondition transformer — wp(C, Q) is the weakest P such that {P} C {Q}. Type: Program → Prop → Prop