Commit 191c8f17 authored by Robbert Krebbers's avatar Robbert Krebbers

Change the level of wand so it is more like the implication.

parent 55a04c5f
......@@ -220,7 +220,7 @@ Infix "→" := uPred_impl : uPred_scope.
Infix "★" := uPred_sep (at level 80, right associativity) : uPred_scope.
Notation "(★)" := uPred_sep (only parsing) : uPred_scope.
Notation "P -★ Q" := (uPred_wand P Q)
(at level 90, Q at level 200, right associativity) : uPred_scope.
(at level 199, Q at level 200, right associativity) : uPred_scope.
Notation "∀ x .. y , P" :=
(uPred_forall (λ x, .. (uPred_forall (λ y, P)) ..)%I) : uPred_scope.
Notation "∃ x .. y , P" :=
......
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