diff options
| author |  Jason Gross <jagro@google.com> | 2018-07-25 10:01:26 -0400 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2018-07-25 10:33:15 -0400 |
| commit | fad8bab9ac50d935f7bf6dd8b940f5c8836b8b77 (patch) | |
| tree | 69a540df937ffb18daf22623687c82b6e994e548 | |
| parent | ea1fd608e7e00d5511a1c8816a5355ab00b810af (diff) | |
Reserve ;;;, fix level of prefix # to not clash with infix #
| -rw-r--r-- | src/Util/Notations.v | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/src/Util/Notations.v b/src/Util/Notations.v index ae9a34533..c010534a5 100644 --- a/src/Util/Notations.v +++ b/src/Util/Notations.v @@ -90,6 +90,7 @@ Reserved Notation "A <--- X ; B" (at level 70, X at next level, right associativ Reserved Notation "A <---- X ; B" (at level 70, X at next level, right associativity, format "'[v' A <---- X ; '/' B ']'"). Reserved Notation "A <----- X ; B" (at level 70, X at next level, right associativity, format "'[v' A <----- X ; '/' B ']'"). Reserved Notation "A ;; B" (at level 70, right associativity, format "'[v' A ;; '/' B ']'"). +Reserved Notation "A ;;; B" (at level 70, right associativity, format "'[v' A ;;; '/' B ']'"). Reserved Notation "u [ i ]" (at level 30). Reserved Notation "v [[ i ]]" (at level 30). Reserved Notation "u {{ i }}" (at level 30). @@ -140,7 +141,13 @@ Reserved Notation "A ~> R" (at level 99). Reserved Notation "A --->" (left associativity, at level 65). Reserved Notation "'return' x" (at level 70, format "'return' x"). Reserved Notation "f x" (only printing, at level 10, left associativity). -Reserved Notation "# x" (at level 0, format "# x"). -Reserved Notation "## x" (at level 0, format "## x"). -Reserved Notation "### x" (at level 0, format "### x"). +(* TODO: Uncomment this block when https://github.com/mit-plv/bbv/pull/13 is merged +Reserved Notation "$ x" (at level 9, x at level 9, format "$ x"). +Reserved Notation "# x" (at level 55, x at level 9, format "# x"). (* 55, so we don't clash with [_ # _] *) + *) +Reserved Notation "## x" (at level 9, x at level 9, format "## x"). +Reserved Notation "### x" (at level 9, x at level 9, format "### x"). Reserved Notation "\ x .. y , t" (at level 200, x binder, y binder, right associativity, format "\ x .. y , '//' t"). + +(* TODO: Remove these when https://github.com/mit-plv/bbv/pull/13 is merged *) +Reserved Notation "# x" (at level 0, format "# x"). |