diff --git a/tests/playground/envtest.lean b/tests/playground/envtest.lean
new file mode 100644
index 0000000000..2b0363af37
--- /dev/null
+++ b/tests/playground/envtest.lean
@@ -0,0 +1,24 @@
+import init.lean.environment
+open Lean
+
+def mkMyExt : IO (EnvExtension (Array Nat)) :=
+registerEnvExtension [1, 2, 3].toArray
+
+@[init mkMyExt]
+constant myExt : EnvExtension (Array Nat) := default _
+
+def showMyExt (env : Environment) : IO Unit :=
+IO.println $ myExt.getState env
+
+def addVal (env : Environment) (n : Nat) : Environment :=
+myExt.modifyState env $ λ as, as.push n
+
+def main : IO Unit :=
+do
+env ← mkEmptyEnvironment,
+showMyExt env,
+let env := addVal env 10,
+showMyExt env,
+let env := addVal env 20,
+showMyExt env,
+pure ()