Commit 3660c994 authored by Ralf Jung's avatar Ralf Jung

turns out we don't need the hv in any of this

parent c435f4d2
Pipeline #9437 passed with stage
in 14 minutes and 34 seconds
......@@ -501,7 +501,7 @@ Proof.
iIntros "?". Show.
Abort.
(* This is specifically crafted such that not having the `hv` in
(* This is specifically crafted such that not having the printing box in
the proofmode notation breaks the output. *)
Local Notation "'TESTNOTATION' '{{' P '|' Q '}' '}'" := (P Q)%I
(format "'TESTNOTATION' '{{' P '|' '/' Q '}' '}'") : bi_scope.
......
......@@ -51,34 +51,34 @@ Reserved Notation "'<subj>' P" (at level 20, right associativity).
(** Update modalities *)
Reserved Notation "|==> Q" (at level 99, Q at level 200, format "|==> Q").
Reserved Notation "P ==∗ Q"
(at level 99, Q at level 200, format "'[hv ' P ==∗ '/' Q ']'").
(at level 99, Q at level 200, format "'[ ' P ==∗ '/' Q ']'").
Reserved Notation "|={ E1 , E2 }=> Q"
(at level 99, E1, E2 at level 50, Q at level 200,
format "|={ E1 , E2 }=> Q").
Reserved Notation "P ={ E1 , E2 }=∗ Q"
(at level 99, E1,E2 at level 50, Q at level 200,
format "'[hv ' P ={ E1 , E2 }=∗ '/' Q ']'").
format "'[ ' P ={ E1 , E2 }=∗ '/' Q ']'").
Reserved Notation "|={ E }=> Q"
(at level 99, E at level 50, Q at level 200,
format "|={ E }=> Q").
Reserved Notation "P ={ E }=∗ Q"
(at level 99, E at level 50, Q at level 200,
format "'[hv ' P ={ E }=∗ '/' Q ']'").
format "'[ ' P ={ E }=∗ '/' Q ']'").
Reserved Notation "|={ E1 , E2 }▷=> Q"
(at level 99, E1, E2 at level 50, Q at level 200,
format "|={ E1 , E2 }▷=> Q").
Reserved Notation "P ={ E1 , E2 }▷=∗ Q"
(at level 99, E1, E2 at level 50, Q at level 200,
format "'[hv ' P ={ E1 , E2 }▷=∗ '/' Q ']'").
format "'[ ' P ={ E1 , E2 }▷=∗ '/' Q ']'").
Reserved Notation "|={ E }▷=> Q"
(at level 99, E at level 50, Q at level 200,
format "|={ E }▷=> Q").
Reserved Notation "P ={ E }▷=∗ Q"
(at level 99, E at level 50, Q at level 200,
format "'[hv ' P ={ E }▷=∗ '/' Q ']'").
format "'[ ' P ={ E }▷=∗ '/' Q ']'").
(** Big Ops *)
Reserved Notation "'[∗' 'list]' k ↦ x ∈ l , P"
......
......@@ -54,35 +54,35 @@ Instance: Params (@wp) 6.
Notation "'WP' e @ s ; E {{ Φ } }" := (wp s E e%E Φ)
(at level 20, e, Φ at level 200,
format "'[hv' 'WP' e '/' @ s ; E {{ Φ } } ']'") : bi_scope.
format "'[' 'WP' e '/' @ s ; E {{ Φ } } ']'") : bi_scope.
Notation "'WP' e @ E {{ Φ } }" := (wp NotStuck E e%E Φ)
(at level 20, e, Φ at level 200,
format "'[hv' 'WP' e '/' @ E {{ Φ } } ']'") : bi_scope.
format "'[' 'WP' e '/' @ E {{ Φ } } ']'") : bi_scope.
Notation "'WP' e @ E ? {{ Φ } }" := (wp MaybeStuck E e%E Φ)
(at level 20, e, Φ at level 200,
format "'[hv' 'WP' e '/' @ E ? {{ Φ } } ']'") : bi_scope.
format "'[' 'WP' e '/' @ E ? {{ Φ } } ']'") : bi_scope.
Notation "'WP' e {{ Φ } }" := (wp NotStuck e%E Φ)
(at level 20, e, Φ at level 200,
format "'[hv' 'WP' e '/' {{ Φ } } ']'") : bi_scope.
format "'[' 'WP' e '/' {{ Φ } } ']'") : bi_scope.
Notation "'WP' e ? {{ Φ } }" := (wp MaybeStuck e%E Φ)
(at level 20, e, Φ at level 200,
format "'[hv' 'WP' e '/' ? {{ Φ } } ']'") : bi_scope.
format "'[' 'WP' e '/' ? {{ Φ } } ']'") : bi_scope.
Notation "'WP' e @ s ; E {{ v , Q } }" := (wp s E e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'[hv' 'WP' e '/' @ s ; E {{ v , Q } } ']'") : bi_scope.
format "'[' 'WP' e '/' @ s ; E {{ v , Q } } ']'") : bi_scope.
Notation "'WP' e @ E {{ v , Q } }" := (wp NotStuck E e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'[hv' 'WP' e '/' @ E {{ v , Q } } ']'") : bi_scope.
format "'[' 'WP' e '/' @ E {{ v , Q } } ']'") : bi_scope.
Notation "'WP' e @ E ? {{ v , Q } }" := (wp MaybeStuck E e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'[hv' 'WP' e '/' @ E ? {{ v , Q } } ']'") : bi_scope.
format "'[' 'WP' e '/' @ E ? {{ v , Q } } ']'") : bi_scope.
Notation "'WP' e {{ v , Q } }" := (wp NotStuck e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'[hv' 'WP' e '/' {{ v , Q } } ']'") : bi_scope.
format "'[' 'WP' e '/' {{ v , Q } } ']'") : bi_scope.
Notation "'WP' e ? {{ v , Q } }" := (wp MaybeStuck e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'[hv' 'WP' e '/' ? {{ v , Q } } ']'") : bi_scope.
format "'[' 'WP' e '/' ? {{ v , Q } } ']'") : bi_scope.
(* Texan triples *)
Notation "'{{{' P } } } e @ s ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
......
......@@ -10,10 +10,10 @@ Arguments Esnoc {_} _%proof_scope _%string _%I.
Notation "" := Enil (only printing) : proof_scope.
Notation "Γ H : P" := (Esnoc Γ (INamed H) P)
(at level 1, P at level 200,
left associativity, format "Γ H : '[hv' P ']' '//'", only printing) : proof_scope.
left associativity, format "Γ H : '[' P ']' '//'", only printing) : proof_scope.
Notation "Γ '_' : P" := (Esnoc Γ (IAnon _) P)
(at level 1, P at level 200,
left associativity, format "Γ '_' : '[hv' P ']' '//'", only printing) : proof_scope.
left associativity, format "Γ '_' : '[' P ']' '//'", only printing) : proof_scope.
Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ∗ Q" :=
(envs_entails (Envs Γ Δ _) Q%I)
......
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