diff --git a/src/bindings/lua/leanlua_state.cpp b/src/bindings/lua/leanlua_state.cpp
index 6095edeee..96c08d953 100644
--- a/src/bindings/lua/leanlua_state.cpp
+++ b/src/bindings/lua/leanlua_state.cpp
@@ -24,6 +24,7 @@ Author: Leonardo de Moura
 #include "bindings/lua/options.h"
 #include "bindings/lua/sexpr.h"
 #include "bindings/lua/format.h"
+#include "bindings/lua/formatter.h"
 #include "bindings/lua/level.h"
 #include "bindings/lua/local_context.h"
 #include "bindings/lua/expr.h"
@@ -173,6 +174,7 @@ struct leanlua_state::imp {
         open_options(m_state);
         open_sexpr(m_state);
         open_format(m_state);
+        open_formatter(m_state);
         open_level(m_state);
         open_local_context(m_state);
         open_expr(m_state);
diff --git a/tests/lua/jst1.lua b/tests/lua/jst1.lua
new file mode 100644
index 000000000..b28d5ec94
--- /dev/null
+++ b/tests/lua/jst1.lua
@@ -0,0 +1,11 @@
+local j1 = mk_assumption_justification(1)
+local j2 = mk_assumption_justification(2)
+assert(is_justification(j1))
+assert(j1:depends_on(j1))
+assert(not j1:depends_on(j2))
+for c in j1:children() do
+   assert(false)
+end
+assert(not j2:has_children())
+print(j1)
+assert(j1:get_main_expr():is_null())