From 2b3bdbe0cfa8ad2bcc65052df4acbd4331b5348e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 26 Mar 2020 12:31:04 -0700
Subject: [PATCH] test: implicit lambdas + notation

---
 tests/lean/run/newfrontend1.lean | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/tests/lean/run/newfrontend1.lean b/tests/lean/run/newfrontend1.lean
index eae8df6248..bd23643334 100644
--- a/tests/lean/run/newfrontend1.lean
+++ b/tests/lean/run/newfrontend1.lean
@@ -301,3 +301,18 @@ def tst1 : {α : Type} → α → α :=
 @(fn α a => a)
 
 #check @tst1
+
+syntax ident "==>" term : term
+
+macro_rules
+| `($x:ident ==> $b) => `(fn $x => $b)
+
+#check x ==> x+1
+
+def tst2 : {α : Type} → α → α :=
+@(α ==> a ==> a)
+
+#check @tst2
+
+def tst3 : {α : Type} → {β : Type} → α → β → α × β :=
+@(α ==> @(β ==> a ==> b ==> (a, b)))