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

fix(frontends/lean/notation_cmd): fixes #585

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-07 08:35:46 -07:00
parent 16b7bc3922
commit 171530d5cc
2 changed files with 12 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/notation_cmd.cpp
View file

@ -168,7 +168,7 @@ static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, nota
}
} else {
auto old_prec = get_precedence(env, tk.c_str(), grp);
if (!old_prec || (k != mixfix_kind::prefix && old_prec != prec))
if (!old_prec || k != mixfix_kind::prefix)
new_token = mk_token_entry(tk.c_str(), *prec, grp);
if (k == mixfix_kind::infixr)
prec = *prec - 1;
@ -267,8 +267,6 @@ static name parse_quoted_symbol_or_token(parser & p, buffer<token_entry> & new_t
if (p.curr_is_token(get_colon_tk())) {
p.next();
unsigned prec = parse_precedence(p);
auto old_prec = get_precedence(env, tkcs, grp);
if (!old_prec || prec != *old_prec)
new_tokens.push_back(mk_token_entry(tkcs, prec, grp));
} else if (!get_precedence(env, tkcs, grp)) {
new_tokens.push_back(mk_token_entry(tkcs, LEAN_DEFAULT_PRECEDENCE, grp));

10
tests/lean/run/585.lean Normal file
View file

@ -0,0 +1,10 @@
import data.finset.basic
open finset
check ∅ -- o.k.
check λs t, subset s t -- o.k.
check λs t, s ⊆ t -- fixed
infix `⊆`:50 := subset
check λs t, s ⊆ t