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

fix(library/init/lean/environment): throw error if environment already contains constant

Browse source
This commit is contained in:
Leonardo de Moura 2019-05-15 09:30:01 -07:00
parent 3193e91aff
commit 89e01368cd
2 changed files with 609 additions and 332 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -390,9 +390,11 @@ do
let const2ModIdx := mods.iterate {} $ λ modIdx (mod : ModuleData) (m : HashMap Name ModuleIdx),
mod.constants.iterate m $ λ _ cinfo m,
m.insert cinfo.name modIdx.val,
let constants := mods.iterate SMap.empty $ λ _ (mod : ModuleData) (cs : SMap Name ConstantInfo Name.quickLt),
mod.constants.iterate cs $ λ _ cinfo cs,
cs.insert cinfo.name cinfo,
constants ← mods.miterate SMap.empty $ λ _ (mod : ModuleData) (cs : SMap Name ConstantInfo Name.quickLt),
mod.constants.miterate cs $ λ _ cinfo cs, do {
when (cs.contains cinfo.name) $ throw (IO.userError ("import failed, environment already contains '" ++ toString cinfo.name ++ "'")),
pure $ cs.insert cinfo.name cinfo
},
let constants := constants.switch,
exts ← mkInitialExtensionStates,
let env : Environment := {

933
src/stage0/init/lean/environment.cpp generated
View file

File diff suppressed because it is too large Load diff