From dcd64fae5a388face9fa8fc8b47d1816625bd424 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 18 Feb 2020 09:18:52 -0800
Subject: [PATCH] test: add new structure instance + implicit lambda tests

---
 tests/lean/run/structInst2.lean | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 tests/lean/run/structInst2.lean

diff --git a/tests/lean/run/structInst2.lean b/tests/lean/run/structInst2.lean
new file mode 100644
index 0000000000..9ea2fa3e13
--- /dev/null
+++ b/tests/lean/run/structInst2.lean
@@ -0,0 +1,11 @@
+import Init.Control.Option
+
+new_frontend
+
+def optMonad {m} [Monad m] : Monad (OptionT m) :=
+{ pure := OptionT.pure, bind := OptionT.bind }
+
+def optAlt {m} [Monad m] : Alternative (OptionT m) :=
+{ failure       := OptionT.fail,
+  orelse        := OptionT.orelse,
+  toApplicative := Monad.toApplicative (OptionT m) } -- TODO: check toApplicative binder annotations