diff options
| author |  Benjamin Barenblat <bbaren@google.com> | 2019-04-26 17:10:05 -0400 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@google.com> | 2019-04-26 17:10:05 -0400 |
| commit | 6de992d169e076f2e579e14b0d64ff68616e04b0 (patch) | |
| tree | 8e9d90a802227b60ed1f4b387ddec8d4084e530d /src/Language.v | |
| parent | 4483d41d6a510e01041f05546643934c9d2a887b (diff) | |
Restore `Reserved Notation` directives for `$ x` and `# x`, which were
commented out to avoid conflicts with bbv. Make both notations `at level
9, x at level 9`, which matches unary prefix operators throughout the
rest of the development.
Diffstat (limited to 'src/Language.v')
| -rw-r--r-- | src/Language.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Language.v b/src/Language.v index eb64e0f2e..b4fc4ed2d 100644 --- a/src/Language.v +++ b/src/Language.v @@ -782,7 +782,7 @@ Module Compilers. Notation "\ x .. y , f" := (Abs (fun x => .. (Abs (fun y => f%expr)) .. )) : expr_scope. Notation "'λ' x .. y , f" := (Abs (fun x => .. (Abs (fun y => f%expr)) .. )) : expr_scope. Notation "'expr_let' x := A 'in' b" := (LetIn A (fun x => b%expr)) : expr_scope. - Notation "'$' x" := (Var x) (at level 10, format "'$' x") : expr_scope. + Notation "'$' x" := (Var x) : expr_scope. Notation "### x" := (Ident x) : expr_scope. End Notations. End expr. |