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