diff --git a/tests/lean/alias3.lean b/tests/lean/alias3.lean
new file mode 100644
index 000000000..52a0ff2c1
--- /dev/null
+++ b/tests/lean/alias3.lean
@@ -0,0 +1,2 @@
+alias A : Bool
+alias A : Nat
\ No newline at end of file
diff --git a/tests/lean/alias3.lean.expected.out b/tests/lean/alias3.lean.expected.out
new file mode 100644
index 000000000..2c4f79c4e
--- /dev/null
+++ b/tests/lean/alias3.lean.expected.out
@@ -0,0 +1,3 @@
+  Set: pp::colors
+  Set: pp::unicode
+Error (line: 2, pos: 13) alias 'A' was already defined