Commit 58ae11ed authored by Robbert Krebbers's avatar Robbert Krebbers

Change the level of `ref` so it's the same as application.

parent 787636f5
Pipeline #15960 passed with stage
in 12 minutes and 22 seconds
......@@ -86,6 +86,14 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
--------------------------------------∗
WP "x" {{ _, True }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
============================
--------------------------------------∗
WP let: "f" := λ: "x", "x" in ref ("f" #10) {{ _, True }}
1 subgoal
Σ : gFunctors
......
......@@ -149,6 +149,12 @@ End tests.
Section printing_tests.
Context `{!heapG Σ}.
Lemma ref_print :
True - WP let: "f" := (λ: "x", "x") in ref ("f" #10) {{ _, True }}.
Proof.
iIntros "_". Show.
Abort.
(* These terms aren't even closed, but that's not what this is about. The
length of the variable names etc. has been carefully chosen to trigger
particular behavior of the Coq pretty printer. *)
......
......@@ -59,8 +59,7 @@ Notation "'match:' e0 'with' 'InjR' x1 => e1 | 'InjL' x2 => e2 'end'" :=
Notation "()" := LitUnit : val_scope.
Notation "! e" := (Load e%E) (at level 9, right associativity) : expr_scope.
Notation "'ref' e" := (Alloc e%E)
(at level 30, right associativity) : expr_scope.
Notation "'ref' e" := (Alloc e%E) (at level 10) : expr_scope.
Notation "- e" := (UnOp MinusUnOp e%E) : expr_scope.
Notation "e1 + e2" := (BinOp PlusOp e1%E e2%E) : expr_scope.
......
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