diff --git a/tests/lean/str1.lean b/tests/lean/str1.lean
new file mode 100644
index 0000000000..e43287a236
--- /dev/null
+++ b/tests/lean/str1.lean
@@ -0,0 +1,34 @@
+import data.list
+
+-- set_option pp.all true
+open string char list
+
+check "ABC"
+
+check str (of_nat 68) (str (of_nat 65) (str (of_nat 66) "abc"))
+
+check list.cons (of_nat 65) "abc"
+
+check list.cons (of_nat 66) (list.cons (of_nat 65) list.nil)
+
+check (of_nat 67)::(of_nat 66)::(of_nat 65)::nil
+
+check (of_nat 68)::"abc"
+
+check append "abc" "cde"
+
+set_option pp.strings false
+
+check "ABC"
+
+check str (of_nat 68) (str (of_nat 65) (str (of_nat 66) "abc"))
+
+check list.cons (of_nat 65) "abc"
+
+check list.cons (of_nat 66) (list.cons (of_nat 65) list.nil)
+
+check (of_nat 67)::(of_nat 66)::(of_nat 65)::nil
+
+check (of_nat 68)::"abc"
+
+check append "abc" "cde"
diff --git a/tests/lean/str1.lean.expected.out b/tests/lean/str1.lean.expected.out
new file mode 100644
index 0000000000..ca4695cdde
--- /dev/null
+++ b/tests/lean/str1.lean.expected.out
@@ -0,0 +1,14 @@
+"ABC" : string
+"abcBAD" : string
+"abcA" : list char
+"AB" : list char
+"ABC" : list char
+"abcD" : list char
+"abc" ++ "cde" : list char
+str 67 (str 66 (str 65 empty)) : string
+str 68 (str 65 (str 66 (str 99 (str 98 (str 97 empty))))) : string
+65 :: str 99 (str 98 (str 97 empty)) : list char
+[66, 65] : list char
+[67, 66, 65] : list char
+68 :: str 99 (str 98 (str 97 empty)) : list char
+str 99 (str 98 (str 97 empty)) ++ str 101 (str 100 (str 99 empty)) : list char