More uses of [iDestruct ty_size_eq].

theories/typing/product.v

@@ -119,12 +119,10 @@ Section product.
     - iNext. iSplitL "H↦1 H1". iExists vl1. by iFrame. iExists vl2. by iFrame.
     - iIntros "Htl [H1 H2]". iDestruct ("Htlclose" with "Htl") as "Htl".
       iDestruct "H1" as (vl1') "[H↦1 H1]". iDestruct "H2" as (vl2') "[H↦2 H2]".
-      iAssert (▷ ⌜length vl1' = ty1.(ty_size)⌝)%I with "[#]" as ">%".
-      { iNext. by iApply ty_size_eq. }
-      iAssert (▷ ⌜length vl2' = ty2.(ty_size)⌝)%I with "[#]" as ">%".
-      { iNext. by iApply ty_size_eq. }
+      iDestruct (ty_size_eq with "H1") as "#>%".
+      iDestruct (ty_size_eq with "H2") as "#>%".
       iCombine "H↦1" "H↦1f" as "H↦1". iCombine "H↦2" "H↦2f" as "H↦2".
-      rewrite !heap_mapsto_vec_op; try by congruence.
+      rewrite !heap_mapsto_vec_op; [|congruence..].
       iDestruct "H↦1" as "[_ H↦1]". iDestruct "H↦2" as "[_ H↦2]".
       iMod ("Hclose2" with "Htl [H2 H↦2]") as "[Htl $]". by iExists _; iFrame.
       iMod ("Hclose1" with "Htl [H1 H↦1]") as "[$$]". by iExists _; iFrame. done.

theories/typing/programs.v

@@ -185,8 +185,7 @@ Section typing_rules.
     wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "% Hown1".
     wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "_ Hown2".
     iMod (Hwrt with "* [] LFT HE HL Hown1") as (l vl) "([% %] & Hl & Hclose)"; first done.
-    subst v1. iAssert (⌜1%nat = ty_size ty⌝%I) with "[#]" as %Hsz.
-    { change (1%nat) with (length [v2]). by iApply ty_size_eq. }
+    subst v1. iDestruct (ty_size_eq with "Hown2") as "#Hsz". iDestruct "Hsz" as %Hsz.
     rewrite <-Hsz in *. destruct vl as [|v[|]]; try done.
     rewrite heap_mapsto_vec_singleton. wp_write.
     rewrite -heap_mapsto_vec_singleton.
@@ -212,8 +211,7 @@ Section typing_rules.
     iIntros (v) "% Hown".
     iMod (Hread with "* [] LFT Htl HE HL Hown") as
         (l vl q) "(% & Hl & Hown & Hclose)"; first done.
-    subst v. iAssert (▷⌜length vl = 1%nat⌝)%I with "[#]" as ">%".
-    { rewrite -Hsz. iApply ty_size_eq. done. }
+    subst v. iDestruct (ty_size_eq with "Hown") as "#>%". rewrite ->Hsz in *.
     destruct vl as [|v [|]]; try done.
     rewrite heap_mapsto_vec_singleton. wp_read.
     iMod ("Hclose" with "Hl") as "($ & $ & Hown2)".

theories/typing/type.v

@@ -444,7 +444,6 @@ Section weakening.
     - iDestruct "HL" as %HL. iPureIntro. intros ??. apply HL.
       rewrite HL12. set_solver.
   Qed.
-
 End weakening.
 
 Hint Resolve subtype_refl eqtype_refl : lrust_typing.

theories/typing/unsafe/cell.v

@@ -34,9 +34,8 @@ Section cell.
     { iMod (na_bor_acc with "LFT Hshr Htok Htl") as "(Hown & Htl & Hclose)"; [solve_ndisj..|].
       iDestruct "Hown" as (vl) "[H↦ #Hown]".
       simpl. assert (F ∖ ∅ = F) as -> by set_solver+.
-      iAssert (▷ ⌜length vl = ty_size ty⌝)%I with "[#]" as ">EQ".
-      { iNext. by iApply ty_size_eq. }
-      rewrite Hsz. iDestruct "EQ" as %EQ. iMod ("Hclose" with "[H↦] Htl") as "[$ $]".
+      iDestruct (ty_size_eq with "Hown") as "#>%". rewrite ->Hsz in *.
+      iMod ("Hclose" with "[H↦] Htl") as "[$ $]".
       { iExists vl. by iFrame. }
       iModIntro. iSplitL "".
       { iNext. iExists vl. destruct vl; last done. iFrame "Hown".
@@ -52,7 +51,6 @@ Section cell.
   Global Instance cell_send :
     Send ty → Send (cell ty).
   Proof. intros. split. simpl. apply send_change_tid. Qed.
-
 End cell.
 
 Section typing.