diff --git a/src/api/ios.cpp b/src/api/ios.cpp
index ef47ee52f..76a7c8d8a 100644
--- a/src/api/ios.cpp
+++ b/src/api/ios.cpp
@@ -7,6 +7,8 @@ Author: Leonardo de Moura
 #include "frontends/lean/pp.h"
 #include "api/string.h"
 #include "api/exception.h"
+#include "api/decl.h"
+#include "api/lean_env.h"
 #include "api/ios.h"
 using namespace lean; // NOLINT
 
@@ -86,3 +88,16 @@ lean_bool lean_ios_reset_diagnostic(lean_ios ios, lean_exception * ex) {
     to_io_state(ios)->set_diagnostic_channel(std::make_shared<string_output_channel>());
     LEAN_CATCH;
 }
+
+lean_bool lean_expr_to_pp_string(lean_env env, lean_ios ios, lean_expr e, char const ** r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(env);
+    check_nonnull(ios);
+    check_nonnull(e);
+    options const & o = to_io_state_ref(ios).get_options();
+    formatter fmt = to_io_state_ref(ios).get_formatter_factory()(to_env_ref(env), o);
+    std::ostringstream out;
+    out << mk_pair(fmt(to_expr_ref(e)), o);
+    *r = mk_string(out.str());
+    LEAN_CATCH;
+}
diff --git a/src/api/lean_ios.h b/src/api/lean_ios.h
index 79715ec23..8ffd693f9 100644
--- a/src/api/lean_ios.h
+++ b/src/api/lean_ios.h
@@ -57,6 +57,9 @@ lean_bool lean_ios_reset_regular(lean_ios ios, lean_exception * ex);
     \pre !lean_ios_is_std(ios) */
 lean_bool lean_ios_reset_diagnostic(lean_ios ios, lean_exception * ex);
 
+/** \brief Store in \c r a pretty printed representation of \c e */
+lean_bool lean_expr_to_pp_string(lean_env env, lean_ios ios, lean_expr e, char const ** r, lean_exception * ex);
+
 /*@}*/
 /*@}*/
 
diff --git a/src/tests/shared/env.c b/src/tests/shared/env.c
index 7b41b23a5..2a72a65f2 100644
--- a/src/tests/shared/env.c
+++ b/src/tests/shared/env.c
@@ -238,16 +238,32 @@ void test_import() {
     lean_options o;
     lean_ios ios;
     lean_env new_env;
+    lean_decl nat_gcd_decl;
+    lean_name nat = mk_name("nat");
+    lean_name nat_gcd;
+    lean_expr nat_gcd_val;
+    char const * s;
     check(lean_options_mk_empty(&o, &ex));
     check(lean_ios_mk_std(o, &ios, &ex));
     check(lean_env_import(env, ios, ms, &new_env, &ex));
     check(lean_env_for_each_decl(new_env, print_decl_name_and_del, &ex));
+
+    check(lean_name_mk_str(nat, "gcd", &nat_gcd, &ex));
+    check(lean_env_get_decl(new_env, nat_gcd, &nat_gcd_decl, &ex));
+    check(lean_decl_get_value(nat_gcd_decl, &nat_gcd_val, &ex));
+    check(lean_expr_to_pp_string(new_env, ios, nat_gcd_val, &s, &ex));
+    printf("nat.gcd\n%s\n", s);
     lean_env_del(env);
     lean_name_del(std);
     lean_list_name_del(ms);
     lean_options_del(o);
     lean_ios_del(ios);
     lean_env_del(new_env);
+    lean_name_del(nat);
+    lean_name_del(nat_gcd);
+    lean_decl_del(nat_gcd_decl);
+    lean_expr_del(nat_gcd_val);
+    lean_string_del(s);
 }
 
 int main() {