Commit dcf68bdf authored by Robbert Krebbers's avatar Robbert Krebbers

Notation and indent.

parent ef76090d
......@@ -52,14 +52,12 @@ Notation "~ᶜ e" := (a_un_op NegOp e%E) (at level 75, right associativity) : ex
Definition a_pre_bin_op (op : bin_op) : val := λ: "x" "y",
"lv" ←ᶜ ("x" ||| "y");;
a_atomic (λ: <>,
"ov" ←ᶜ (∗ᶜ (a_ret (Fst "lv")));;
a_store (a_ret (Fst "lv"))
(a_bin_op op (a_ret "ov") (a_ret (Snd "lv")));;
a_atomic (λ: <>,
"ov" ←ᶜ ∗ᶜ (a_ret (Fst "lv"));;
a_ret (Fst "lv") = a_bin_op op (a_ret "ov") (a_ret (Snd "lv"));;
a_ret "ov").
Notation "e1 +=ᶜ e2" := (a_pre_bin_op PlusOp e1%E e2%E) (at level 80) : expr_scope.
(* M () *)
(* The eta expansion is used to turn it into a value *)
Definition a_seq : val := λ: <>,
......
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