Commit b33a29de authored by Robbert Krebbers's avatar Robbert Krebbers

Notation `P ={E1,E2}▷=∗^n Q`.

parent 66483b1d
...@@ -90,6 +90,9 @@ Reserved Notation "P ={ E }▷=∗ Q" ...@@ -90,6 +90,9 @@ Reserved Notation "P ={ E }▷=∗ Q"
Reserved Notation "|={ E1 , E2 }▷=>^ n Q" Reserved Notation "|={ E1 , E2 }▷=>^ n Q"
(at level 99, E1, E2 at level 50, n at level 9, Q at level 200, (at level 99, E1, E2 at level 50, n at level 9, Q at level 200,
format "|={ E1 , E2 }▷=>^ n Q"). format "|={ E1 , E2 }▷=>^ n Q").
Reserved Notation "P ={ E1 , E2 }▷=∗^ n Q"
(at level 99, E1, E2 at level 50, n at level 9, Q at level 200,
format "P ={ E1 , E2 }▷=∗^ n Q").
(** Big Ops *) (** Big Ops *)
Reserved Notation "'[∗' 'list]' k ↦ x ∈ l , P" Reserved Notation "'[∗' 'list]' k ↦ x ∈ l , P"
......
...@@ -33,6 +33,8 @@ Notation "P ={ E1 , E2 }▷=∗ Q" := (P -∗ |={ E1 , E2, E1 }▷=> Q)%I : bi_s ...@@ -33,6 +33,8 @@ Notation "P ={ E1 , E2 }▷=∗ Q" := (P -∗ |={ E1 , E2, E1 }▷=> Q)%I : bi_s
Notation "|={ E }▷=> Q" := (|={E,E}=> Q)%I : bi_scope. Notation "|={ E }▷=> Q" := (|={E,E}=> Q)%I : bi_scope.
Notation "P ={ E }▷=∗ Q" := (P ={E,E}= Q)%I : bi_scope. Notation "P ={ E }▷=∗ Q" := (P ={E,E}= Q)%I : bi_scope.
Notation "|={ E1 , E2 }▷=>^ n Q" := (Nat.iter n (λ P, |={E1,E2}=> P) Q)%I : bi_scope. Notation "|={ E1 , E2 }▷=>^ n Q" := (Nat.iter n (λ P, |={E1,E2}=> P) Q)%I : bi_scope.
Notation "P ={ E1 , E2 }▷=∗^ n Q" := (P |={E1,E2}=>^n Q)%I (only parsing) : stdpp_scope.
Notation "P ={ E1 , E2 }▷=∗^ n Q" := (P - |={E1,E2}=>^n Q)%I : bi_scope.
(** Bundled versions *) (** Bundled versions *)
(* Mixins allow us to create instances easily without having to use Program *) (* Mixins allow us to create instances easily without having to use Program *)
......
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