add a test

Author: hargoniX

tests/lean/run/eta_lambda_lift.lean

@@ -0,0 +1,17 @@
+import Lean.Util.FindExpr
+
+/-!
+This test asserts that the compiler will eta contract trivial lambdas instead of lambda lifting
+them.
+-/
+
+/--
+trace: [Compiler.lambdaLifting] size: 2
+    def test e : Option Lean.Expr :=
+      let _f.1 := Lean.Expr.hasMVar;
+      let _x.2 := Lean.Expr.findImpl? _f.1 e;
+      return _x.2
+-/
+#guard_msgs in
+set_option trace.Compiler.lambdaLifting true in
+def test (e : Lean.Expr) := e.find? (fun e => e.hasMVar)