From 4e307f906fdd24faa311591519db66312f14b970 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 9 Aug 2016 16:50:36 -0700
Subject: [PATCH] fix(library/init/function): '$' notation should be
 left-associative

---
 library/init/function.lean             | 2 +-
 tests/lean/notation8.lean              | 5 +++++
 tests/lean/notation8.lean.expected.out | 2 ++
 3 files changed, 8 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/notation8.lean
 create mode 100644 tests/lean/notation8.lean.expected.out

diff --git a/library/init/function.lean b/library/init/function.lean
index 38a3e52089..eae841a173 100644
--- a/library/init/function.lean
+++ b/library/init/function.lean
@@ -8,7 +8,7 @@ General operations on functions.
 prelude
 import init.prod init.funext init.logic
 
-notation f ` $ `:1 a:0 := f a
+notation f ` $ `:1 a:1 := f a
 
 variables {A : Type} {B : Type} {C : Type} {D : Type} {E : Type}
 
diff --git a/tests/lean/notation8.lean b/tests/lean/notation8.lean
new file mode 100644
index 0000000000..53323448cd
--- /dev/null
+++ b/tests/lean/notation8.lean
@@ -0,0 +1,5 @@
+constant f : nat → nat → nat
+constant g : nat → nat
+
+check f $ 1 + g 1 $ g 2 + 2
+check f $ g 1 $ (f $ 1 + 1 $ g 2)
diff --git a/tests/lean/notation8.lean.expected.out b/tests/lean/notation8.lean.expected.out
new file mode 100644
index 0000000000..1d53c321e0
--- /dev/null
+++ b/tests/lean/notation8.lean.expected.out
@@ -0,0 +1,2 @@
+f (1 + g 1) (g 2 + 2) : ℕ
+f (g 1) (f (1 + 1) (g 2)) : ℕ