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

fix: parseImports': respect prelude

Browse source
This commit is contained in:
Sebastian Ullrich 2022-11-15 10:36:40 +01:00 • committed by Leonardo de Moura
parent e3b83625f2
commit 3d1ff59f11
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Lean/Elab/ParseImportsFast.lean
View file

@ -118,9 +118,6 @@ partial def whitespace : Parser := fun input s =>
@[inline] partial def keyword (k : String) : Parser :=
keywordCore k (fun _ s => s.mkError s!"`{k}` expected") (fun _ s => s)
@[inline] partial def keywordOpt (k : String) : Parser :=
keywordCore k (fun _ s => s) (fun _ s => s)
@[inline] def isIdCont : String → State → Bool := fun input s =>
let i := s.pos
let curr := input.get i
@ -186,8 +183,11 @@ partial def moduleIdent (runtimeOnly : Bool) : Parser := fun input s =>
| none => many p input s
| some _ => { pos, error? := none, imports := s.imports.shrink size }
@[inline] partial def preludeOpt (k : String) : Parser :=
keywordCore k (fun _ s => s.pushModule `Init false) (fun _ s => s)
def main : Parser :=
keywordOpt "prelude" >>
preludeOpt "prelude" >>
many (keyword "import" >> keywordCore "runtime" (moduleIdent false) (moduleIdent true))
end ParseImports