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

feat(frontends/lean/notation_cmd): allow 'max' to use as a precedence level

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-01 16:46:32 -07:00
parent 4cb5f97038
commit 8cdf44b87b
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/frontends/lean/notation_cmd.cpp
View file

@ -183,7 +183,7 @@ static void parse_notation_local(parser & p, buffer<expr> & locals) {
static action parse_action(parser & p, name const & prev_token, buffer<expr> & locals, buffer<token_entry> & new_tokens) {
if (p.curr_is_token(g_colon)) {
p.next();
if (p.curr_is_numeral()) {
if (p.curr_is_numeral() || p.curr_is_token_or_id(g_max)) {
unsigned prec = parse_precedence(p, "invalid notation declaration, small numeral expected");
return mk_expr_action(prec);
} else if (p.curr_is_string()) {