diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 695932d48..75d4acf62 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -4,11 +4,31 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "library/io_state_stream.h"
 #include "frontends/lean/parser.h"
 
 namespace lean {
+environment print_cmd(parser & p) {
+    if (p.curr() == scanner::token_kind::String) {
+        regular(p.env(), p.ios()) << p.get_str_val() << "\n";
+        p.next();
+    } else {
+        throw parser_error("invalid print command", p.pos());
+    }
+    return p.env();
+}
+
+cmd_table init_cmd_table() {
+    cmd_table r;
+    add_cmd(r, cmd_info("print", "print a string", print_cmd));
+    return r;
+}
+
 cmd_table get_builtin_cmds() {
-    return cmd_table();
+    static optional<cmd_table> r;
+    if (!r)
+        r = init_cmd_table();
+    return *r;
 }
 }
 
diff --git a/src/frontends/lean/cmd_table.h b/src/frontends/lean/cmd_table.h
index 0fb6b45f2..a0132059b 100644
--- a/src/frontends/lean/cmd_table.h
+++ b/src/frontends/lean/cmd_table.h
@@ -35,4 +35,6 @@ typedef cmd_info_tmpl<tactic_command_fn> tactic_cmd_info;
 
 typedef rb_map<name, cmd_info,        name_quick_cmp> cmd_table;
 typedef rb_map<name, tactic_cmd_info, name_quick_cmp> tactic_cmd_table;
+
+inline void add_cmd(cmd_table & t, cmd_info const & cmd) { t.insert(cmd.get_name(), cmd); }
 }
diff --git a/tests/lean/t2.lean b/tests/lean/t2.lean
new file mode 100644
index 000000000..19f8e82c6
--- /dev/null
+++ b/tests/lean/t2.lean
@@ -0,0 +1,2 @@
+print "hello world"
+print "testing"
diff --git a/tests/lean/t2.lean.expected.out b/tests/lean/t2.lean.expected.out
new file mode 100644
index 000000000..32eab3e59
--- /dev/null
+++ b/tests/lean/t2.lean.expected.out
@@ -0,0 +1,2 @@
+hello world
+testing