diff --git a/tests/lua/mod1.lua b/tests/lua/mod1.lua
new file mode 100644
index 000000000..f7ad7ef5b
--- /dev/null
+++ b/tests/lua/mod1.lua
@@ -0,0 +1,21 @@
+local env = environment()
+env = add_decl(env, mk_var_decl("A", Bool))
+local A  = Const("A")
+env = add_decl(env, mk_axiom("H1", A))
+local H1 = Const("H1")
+env = add_decl(env, mk_theorem("H2", A, H1))
+assert(env:get("H2"):is_theorem())
+env = add_decl(env, mk_definition("B", Bool, A))
+env:export("mod1_mod.olean")
+
+local env2 = import_modules("mod1_mod.olean")
+assert(env2:get("A"):type() == Bool)
+assert(env2:get("A"):is_var_decl())
+assert(env2:get("H1"):type() == A)
+assert(env2:get("H1"):is_axiom())
+assert(env2:get("H2"):type() == A)
+assert(env2:get("H2"):is_theorem())
+assert(env2:get("H2"):value() == H1)
+assert(env2:get("B"):type() == Bool)
+assert(env2:get("B"):value() == A)
+assert(env2:get("B"):is_definition())