From 25879c97fa750c05c1b82500a77a204bcd5ecf72 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 11 May 2019 17:53:27 -0700 Subject: [PATCH] test(tests/playground/envtest): add small environment extension test --- tests/playground/envtest.lean | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 tests/playground/envtest.lean 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 ()