From dc93bc37ccbd2670f672d7cd774ca9d7185b49ea Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 22 Mar 2019 17:28:25 +0100 Subject: [PATCH] chore(tests/playground/environment_ext): fix --- tests/playground/environment_ext.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/tests/playground/environment_ext.lean b/tests/playground/environment_ext.lean index b82728007e..f74769dd91 100644 --- a/tests/playground/environment_ext.lean +++ b/tests/playground/environment_ext.lean @@ -1,4 +1,4 @@ -import init.Lean init.Lean.Parser.Syntax +import init.lean init.lean.parser.syntax namespace Lean /-- An extension of the State held by an `environment` object. The new State @@ -62,15 +62,15 @@ structure attributeInfo := (scopedExt : environmentExt attributeEntry (List attributeEntry)) namespace attributeInfo -def addScopedEntry (attr : attributeInfo) : attributeEntry → environment → environment := attr.scopedExt.addEntry ff +def addScopedEntry (attr : attributeInfo) : attributeEntry → environment → environment := attr.scopedExt.addEntry false def activateScopedEntries (attr : attributeInfo) (declOpen : Name → Bool) (env : environment) : environment := -((attr.scopedExt.getState env).filter (λ e : attributeEntry, declOpen e.Decl)).foldr (attr.addActiveEntry tt) env +((attr.scopedExt.getState env).filter (λ e : attributeEntry, declOpen e.Decl)).foldr (attr.addActiveEntry true) env end attributeInfo -def attributesRef.init : IO (IO.ref (List attributeInfo)) := IO.mkRef [] -@[init attributesRef.init] private constant attributesRef : IO.ref (List attributeInfo) := default _ +def attributesRef.init : IO (IO.Ref (List attributeInfo)) := IO.mkRef [] +@[init attributesRef.init] private constant attributesRef : IO.Ref (List attributeInfo) := default _ /-- The List of all attributes registered by `attributeExt.register`. -/ -def attributes : IO (List attributeInfo) := attributesRef.read +def attributes : IO (List attributeInfo) := attributesRef.get namespace attributeExt variable {stateTy : Type}