diff --git a/tests/lean/toExpr.lean b/tests/lean/toExpr.lean
new file mode 100644
index 0000000000..8162191b53
--- /dev/null
+++ b/tests/lean/toExpr.lean
@@ -0,0 +1,21 @@
+import Lean
+
+open Lean BitVec
+
+open Meta in
+def test [ToExpr α] (a : α) : MetaM Unit := do
+  let e := toExpr a
+  let type ← inferType e
+  check e
+  logInfo m!"{e} : {type}"
+
+run_meta test (2 : Fin 4)
+run_meta test (8 : Fin 5)
+run_meta test (300#8)
+run_meta test (300#32)
+run_meta test (58#8)
+run_meta test (20 : UInt8)
+run_meta test (30 : UInt16)
+run_meta test (40 : UInt32)
+run_meta test (50 : UInt64)
+run_meta test (60 : USize)
diff --git a/tests/lean/toExpr.lean.expected.out b/tests/lean/toExpr.lean.expected.out
new file mode 100644
index 0000000000..0b5cec68bc
--- /dev/null
+++ b/tests/lean/toExpr.lean.expected.out
@@ -0,0 +1,10 @@
+2 : Fin 4
+3 : Fin 5
+44#8 : BitVec 8
+300#32 : BitVec 32
+58#8 : BitVec 8
+20 : UInt8
+30 : UInt16
+40 : UInt32
+50 : UInt64
+60 : USize