Commit 2d44c0ef authored by Robbert Krebbers's avatar Robbert Krebbers

Remove weird notation for par.

parent bf42c065
Pipeline #2292 passed with stage
......@@ -8,8 +8,7 @@ Definition par : val :=
let: "v2" := Snd "fs" #() in
let: "v1" := join "handle" in
Pair "v1" "v2".
Notation Par e1 e2 := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E.
Infix "||" := Par : expr_scope.
Notation "e1 || e2" := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E : expr_scope.
Global Opaque par.
Section proof.
......
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