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

fix: typo

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-21 11:44:26 -07:00
parent 0de92b069f
commit c9e902034d
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Environment.lean
View file

@ -519,7 +519,7 @@ partial def importModulesAux : List Import → (NameSet × Array ModuleData × A
let regions := regions.push region;
importModulesAux is (s, mods, regions)
private partial def getEntriesFor (mod : ModuleData) (extId : Name) : Nat → Array EnvExtensionState
private partial def getEntriesFor (mod : ModuleData) (extId : Name) : Nat → Array EnvExtensionEntry
| i =>
if i < mod.entries.size then
let curr := mod.entries.get! i;