From 171530d5cc9100fe06d09022ebcc5c0260834815 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 7 May 2015 08:35:46 -0700 Subject: [PATCH] fix(frontends/lean/notation_cmd): fixes #585 --- src/frontends/lean/notation_cmd.cpp | 6 ++---- tests/lean/run/585.lean | 10 ++++++++++ 2 files changed, 12 insertions(+), 4 deletions(-) create mode 100644 tests/lean/run/585.lean diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp index 5c9c6b7da..c4d428a3b 100644 --- a/src/frontends/lean/notation_cmd.cpp +++ b/src/frontends/lean/notation_cmd.cpp @@ -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,9 +267,7 @@ static name parse_quoted_symbol_or_token(parser & p, buffer & 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)); + 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)); used_default = true; diff --git a/tests/lean/run/585.lean b/tests/lean/run/585.lean new file mode 100644 index 000000000..73f33362e --- /dev/null +++ b/tests/lean/run/585.lean @@ -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