fix(library/init/function): '$' notation should be left-associative

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}
 

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)

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)) : ℕ