Commit ce5f7710 authored by Robbert Krebbers's avatar Robbert Krebbers

Also use %E scopes in notations for Hoare triples.

parent ae01dd71
......@@ -6,29 +6,29 @@ Definition ht `{irisG Λ Σ} (E : coPset) (P : iProp Σ)
( (P WP e @ E {{ Φ }}))%I.
Instance: Params (@ht) 4.
Notation "{{ P } } e @ E {{ Φ } }" := (ht E P e Φ)
Notation "{{ P } } e @ E {{ Φ } }" := (ht E P e%E Φ)
(at level 20, P, e, Φ at level 200,
format "{{ P } } e @ E {{ Φ } }") : uPred_scope.
Notation "{{ P } } e {{ Φ } }" := (ht P e Φ)
Notation "{{ P } } e {{ Φ } }" := (ht P e%E Φ)
(at level 20, P, e, Φ at level 200,
format "{{ P } } e {{ Φ } }") : uPred_scope.
Notation "{{ P } } e @ E {{ Φ } }" := (True ht E P e Φ)
Notation "{{ P } } e @ E {{ Φ } }" := (True ht E P e%E Φ)
(at level 20, P, e, Φ at level 200,
format "{{ P } } e @ E {{ Φ } }") : C_scope.
Notation "{{ P } } e {{ Φ } }" := (True ht P e Φ)
Notation "{{ P } } e {{ Φ } }" := (True ht P e%E Φ)
(at level 20, P, e, Φ at level 200,
format "{{ P } } e {{ Φ } }") : C_scope.
Notation "{{ P } } e @ E {{ v , Q } }" := (ht E P e (λ v, Q))
Notation "{{ P } } e @ E {{ v , Q } }" := (ht E P e%E (λ v, Q))
(at level 20, P, e, Q at level 200,
format "{{ P } } e @ E {{ v , Q } }") : uPred_scope.
Notation "{{ P } } e {{ v , Q } }" := (ht P e (λ v, Q))
Notation "{{ P } } e {{ v , Q } }" := (ht P e%E (λ v, Q))
(at level 20, P, e, Q at level 200,
format "{{ P } } e {{ v , Q } }") : uPred_scope.
Notation "{{ P } } e @ E {{ v , Q } }" := (True ht E P e (λ v, Q))
Notation "{{ P } } e @ E {{ v , Q } }" := (True ht E P e%E (λ v, Q))
(at level 20, P, e, Q at level 200,
format "{{ P } } e @ E {{ v , Q } }") : C_scope.
Notation "{{ P } } e {{ v , Q } }" := (True ht P e (λ v, Q))
Notation "{{ P } } e {{ v , Q } }" := (True ht P e%E (λ v, Q))
(at level 20, P, e, Q at level 200,
format "{{ P } } e {{ v , Q } }") : C_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