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

feat(library/init/lean/elaborator): name lookup for universes

Browse source
This commit is contained in:
Sebastian Ullrich 2018-12-11 19:01:56 +01:00
parent 94dec2cb9f
commit 009e499e95
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
library/init/lean/elaborator.lean
View file

@ -113,11 +113,14 @@ def level_add : level → nat → level
def to_level : syntax → elaborator_m level
| stx := do
(fn, args) ← level_get_app_args stx,
st ← get,
match fn.kind with
| some level.leading := (match view level.leading stx, args with
| level.leading.view.hole _, [] := pure $ level.mvar "u" -- TODO(Sebastian): name?
| level.leading.view.lit lit, [] := pure $ level.of_nat lit.to_nat
| level.leading.view.var id, [] := pure $ level.param $ mangle_ident id
| level.leading.view.var id, [] := let id := mangle_ident id in (match st.local_state.univs.find id with
| some _ := pure $ level.param id
| none := error stx $ "unknown universe variable '" ++ to_string id ++ "'")
| level.leading.view.max _, (arg::args) := list.foldl level.max <$> to_level arg <*> args.mmap to_level
| level.leading.view.imax _, (arg::args) := list.foldl level.imax <$> to_level arg <*> args.mmap to_level
| _, _ := error stx "ill-formed universe level")