From 182775aa4f00514719ffb815881e44b9d02f868a Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Wed, 11 Dec 2024 14:43:30 +0000
Subject: [PATCH] deriving test cases

The final test case currently fails, exposing a bug when auto implicits are disabled
---
 tests/lean/run/derivingToExpr.lean | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)
 create mode 100644 tests/lean/run/derivingToExpr.lean

diff --git a/tests/lean/run/derivingToExpr.lean b/tests/lean/run/derivingToExpr.lean
new file mode 100644
index 000000000000..c3504075ccb1
--- /dev/null
+++ b/tests/lean/run/derivingToExpr.lean
@@ -0,0 +1,22 @@
+import Lean.Elab.Deriving.ToExpr
+
+open Lean (ToExpr)
+
+-- Test with a universe polymporphic type parameter
+inductive Option' (α : Type u)
+  | some (a : α)
+  | none
+  deriving ToExpr
+
+-- Test with recursive type
+inductive List' (α : Type u)
+  | cons (a : α) (as : List' α)
+  | nil
+  deriving ToExpr
+
+-- Test without (universe) auto implicit
+set_option autoImplicit false in
+inductive ExplicitList'.{u} (α : Type u)
+  | cons (a : α) (as : List' α)
+  | nil
+  deriving ToExpr