Make memcpy a value and make it Opaque.

This reduces the compilation time of mempcy.v from 7m to 8s.

Also, avoid unfolding wexpr and wexpr' which create a term whose size is
28497 lines when shown with Set Printing All. (Even pretty printing took
ages!)

memcpy.v

 From lrust Require Export notation.
 From lrust Require Import heap proofmode.
 
-Definition memcpy : expr [] :=
+Definition memcpy : val :=
   (rec: "memcpy" ["dst";"len";"src"] :=
      if: '"len" ≤ #0 then #()
      else '"dst" +ₗ #0 <- * ('"src" +ₗ #0);;
           '"memcpy" ['"dst" +ₗ #1 ; '"len" - #1 ; '"src" +ₗ #1]).
+Opaque memcpy.
 
-Notation "e1 <-{ n } * e2" := (^ memcpy [e1%RustE ; #(LitInt n) ; e2%RustE])%RustE
+Notation "e1 <-{ n } * e2" := (memcpy [e1%RustE ; #(LitInt n) ; e2%RustE])%RustE
   (at level 80) : lrust_expr_scope.
 
 Lemma wp_memcpy `{heapG Σ} N E l1 l2 vl1 vl2 q n Φ:
@@ -17,7 +18,7 @@ Lemma wp_memcpy `{heapG Σ} N E l1 l2 vl1 vl2 q n Φ:
   ▷ (l1 ↦★ vl2 ★ l2 ↦★{q} vl2 ={E}=★ Φ #())
   ⊢ WP #l1 <-{n} *#l2 @ E {{ v, Φ v }}.
 Proof.
-  rewrite /memcpy /wexpr' /wexpr /=. iIntros (? Hvl1 Hvl2) "(#Hinv&Hl1&Hl2&HΦ)".
+  iIntros (? Hvl1 Hvl2) "(#Hinv&Hl1&Hl2&HΦ)".
   iLöb (n l1 l2 vl1 vl2 Hvl1 Hvl2) as "IH". wp_rec. wp_op=> ?; wp_if.
   - iApply "HΦ". assert (n = O) by lia; subst; destruct vl1, vl2; try discriminate. by iFrame.
   - revert Hvl1 Hvl2. destruct vl1 as [|v1 vl1], vl2 as [|v2 vl2], n as [|n]; try discriminate.
@@ -27,5 +28,5 @@ Proof.
     replace (Z.pos (Pos.of_succ_nat n)) with (n+1) by lia.
     do 3 wp_op. rewrite Z.add_simpl_r.
     iApply ("IH" with "[%] [%] Hl1 Hl2"); try done.
-    iNext; iIntros "[Hl1 Hl2]"; iApply "HΦ"; by iFrame.
+    iIntros "> [Hl1 Hl2]"; iApply "HΦ"; by iFrame.
 Qed.