curry the first function

theories/examples/refinements/examples.v

@@ -10,8 +10,8 @@ Set Default Proof Using "Type".
 Section implementation.
 
   (* first examples *)
-  Definition first (p: val) : val :=
-    rec: "first" "x" := if: p "x" then "x" else "first" ("x" + #1).
+  Definition first : val :=
+    rec: "first" "p" "x" := if: "p" "x" then "x" else "first" "p" ("x" + #1).
 
   Definition f_ex : val :=
     λ: "x", #41 ≤ "x" - #1.
@@ -60,8 +60,9 @@ Section first_proofs.
     intros Hfg. iStartProof. iRevert (m). iLöb as "IH".
     iIntros (m K) "!# Hsrc Hna".
     iApply (rwp_take_step with "[Hna]"); first done; last first.
-    { rewrite /first. src_pure _ in "Hsrc". fold (first g). iApply weak_src_update_return. iExact "Hsrc". }
-    iIntros "Hsrc". wp_rec. wp_bind (f _).
+    { rewrite /first. src_pure _ in "Hsrc". fold (first). iApply weak_src_update_return. iExact "Hsrc". }
+    iIntros "Hsrc". wp_rec. wp_pures. wp_bind (f _).
+    do 2 src_pure _ in "Hsrc".
     src_bind (g _) in "Hsrc".
     iPoseProof (Hfg with "Hsrc Hna") as "Hfg".
     iApply (rwp_wand with "Hfg"). iIntros (v) "[Hna [Hsrc H]]".