title: Some questions about weakest pre-condition notation in the F* tutorial
body: <p>Chapter 9 in the <a href="https://www.fstar-lang.org/tutorial/" rel="nofollow noreferrer">F* tutorial</a> has an example:</p>
  
  <pre><code>b ::= x | true | false
  e ::= b | let x = e1 in e2 | assert b | if b then e1 else e2
  
  WP b P                      = P b
  WP (let x = e1 in e2) P     = WP e1 (fun x -&gt; WP e2 P)
  WP (assert b) P             = b /\ P b
  WP (if b then e1 else e2) P = (b ==&gt; WP e1 P) /\ ((not b) ==&gt; WP e2 P)
  </code></pre>
  
  <p>Could someone please explain the notation here? I understand that <code>WP</code> is pre-condition and <code>P</code> post-condition, but what is <code>P b</code>? Post-condition that is applied to <code>b</code>?</p>