test(tests/playground/envtest): add small environment extension test

This commit is contained in:
Leonardo de Moura 2019-05-11 17:53:27 -07:00
parent f1d16c261d
commit 25879c97fa

View file

@ -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 ()