Commit 247dfa43 authored by Robbert Krebbers's avatar Robbert Krebbers

Remove spurious type class argument in sort protocol.

parent 8e80459a
Pipeline #20508 failed with stage
in 0 seconds
......@@ -45,8 +45,7 @@ Definition sort_client_func : val := λ: "cmp" "xs",
Section sort.
Context `{!heapG Σ, !proto_chanG Σ}.
Definition sort_protocol {A} (I : A val iProp Σ) (R : A A Prop)
`{!RelDecision R, !Total R} : iProto Σ :=
Definition sort_protocol {A} (I : A val iProp Σ) (R : A A Prop) : iProto Σ :=
(<!> (xs : list A) (l : loc), MSG #l {{ llist I l xs }};
<?> (xs' : list A), MSG #() {{ Sorted R xs' xs' xs llist I l xs' }};
END)%proto.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment