Generalize list_sort_elem to arbitrary types.

6b41f71f · Robbert Krebbers · 353e65d6 · 6b41f71f · 6b41f71f
Commit 6b41f71f authored Jun 28, 2019 by Robbert Krebbers
Expand all Hide whitespace changes
Inline Side-by-side

Showing with 200 additions and 302 deletions

theories/examples/list_sort_elem.v theories/examples/list_sort_elem.v +200 -300

theories/examples/loop_sort.v theories/examples/loop_sort.v +0 -2

No files found.
--- a/theories/examples/list_sort_elem.v
+++ b/theories/examples/list_sort_elem.v
--- a/theories/examples/loop_sort.v
+++ b/theories/examples/loop_sort.v
@@ -16,7 +16,6 @@ Definition loop_sort_service : val :=
 Section loop_sort.
  Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).

-  
  Definition loop_sort_protocol_aux (rec : iProto Σ) : iProto Σ :=
    ((sort_protocol <++> rec) <+> ((<?> c, MSG c {{ c ↣ rec @ N }}; rec) <+> END))%proto.

@@ -48,5 +47,4 @@ Section loop_sort.
      by wp_apply ("IH" with "Hc").
    - by iApply "HΨ".
  Qed.
-
 End loop_sort.
\ No newline at end of file