max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/init/lean/environment): process entries using the order they were inserted

Browse source
This commit is contained in:
Leonardo de Moura 2019-05-14 12:53:50 -07:00
parent a24a1562ea
commit 5e2111f4a4
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/lean/environment.lean
View file

@ -189,7 +189,7 @@ ext.toEnvExtension.modifyState env $ λ s,
def forceStateAux {α σ : Type} (ext : PersistentEnvExtension α σ) (s : PersistentEnvExtensionState α σ) : σ :=
match s.state with
| some d := d
| none := s.entries.foldl (ext.addEntryFn false) s.importedState.get
| none := s.entries.foldr (λ a s, ext.addEntryFn false s a) s.importedState.get
def forceState {α σ : Type} (ext : PersistentEnvExtension α σ) (env : Environment) : Environment :=
ext.toEnvExtension.modifyState env $ λ s, { state := some (ext.forceStateAux s), .. s }
@ -301,7 +301,7 @@ let entries : Array (Name × Array EnvExtensionEntry) := pExts.size.fold
let entryList := (pExts.get i).getEntries env in
let toArrayFn := (pExts.get i).toArrayFn in
let extName := (pExts.get i).name in
result.push (extName, toArrayFn entryList))
result.push (extName, toArrayFn entryList.reverse))
Array.empty,
bytes ← serializeModifications (modListExtension.getState env),
pure {