diff --git a/tests/lua/parser2.lua b/tests/lua/parser2.lua
new file mode 100644
index 000000000..94514100b
--- /dev/null
+++ b/tests/lua/parser2.lua
@@ -0,0 +1,26 @@
+local env = environment()
+parse_lean_cmds([[
+   Variable N : Type
+   Variables x y : N
+   Variable f : N -> N -> N
+   Set pp::colors false
+]], env)
+local f, x, y = Consts("f, x, y")
+print(env:check_type(f(x, y)))
+assert(env:check_type(f(x, y)) == Const("N"))
+assert(not get_options():get{"pp", "colors"})
+parse_lean_cmds([[
+   Set pp::colors true
+]], env)
+assert(get_options():get{"pp", "colors"})
+local o = get_options()
+o:update({"lean", "pp", "notation"}, false)
+assert(not o:get{"lean", "pp", "notation"})
+o = parse_lean_cmds([[
+   Check fun x : N, y
+   Set pp::notation true
+   Check fun x : N, y
+]], env, o)
+print(o)
+assert(o:get{"lean", "pp", "notation"})
+assert(parse_lean("f x y", env) == f(x, y))