Commit 00d7fbc1 authored by Robbert Krebbers's avatar Robbert Krebbers

Proper pretty printing of new `|={E,E'}▷=>^n` notation.

parent 82d7488b
......@@ -88,7 +88,8 @@ Reserved Notation "P ={ E }▷=∗ Q"
(at level 99, E at level 50, Q at level 200,
format "'[' P '/' ={ E }▷=∗ 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").
(** Big Ops *)
Reserved Notation "'[∗' 'list]' k ↦ x ∈ l , 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