michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean/parser): universe declarations

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-29 13:15:09 -08:00
parent f8b82d854e
commit b1efdac07b
1 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/frontends/lean/parser.cpp
View file

@ -2545,6 +2545,13 @@ class parser::imp {
parse_macro(m.m_arg_kinds, m.m_fn, m.m_precedence, args, p);
}
void parse_universe() {
next();
name id = check_identifier_next("invalid universe declaration, identifier expected");
level lvl = parse_level();
m_env->add_uvar(id, lvl);
}
/** \brief Parse a Lean command. */
bool parse_command() {
m_elaborator.clear();
@ -2597,6 +2604,8 @@ class parser::imp {
parse_pop();
} else if (cmd_id == g_end_scope_kwd) {
parse_end_scope();
} else if (cmd_id == g_universe_kwd) {
parse_universe();
} else if (m_cmd_macros && m_cmd_macros->find(cmd_id) != m_cmd_macros->end()) {
parse_cmd_macro(cmd_id, m_last_cmd_pos);
} else {