From 95fbefc1cf32ee8b0513397ea80031338cad509d Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Tue, 15 Mar 2022 16:42:24 +0000 Subject: [PATCH] allow non-local terms The exception only says closed terms are a problem, I want to test what happens if I allow non-local terms as well to see if the docstring needs editing --- src/frontends/lean/user_notation.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontends/lean/user_notation.cpp b/src/frontends/lean/user_notation.cpp index fc5363a69e..fcb2d5ab65 100644 --- a/src/frontends/lean/user_notation.cpp +++ b/src/frontends/lean/user_notation.cpp @@ -76,7 +76,7 @@ static environment add_user_notation(environment const & env, name const & d, un auto pos = p.pos(); expr e = p.parse_expr(get_max_prec()); data.push(p.new_ast("expr", pos).push(p.get_id(e)).m_id); - if (!closed(e) || has_local(e)) { + if (!closed(e)) { throw elaborator_exception(e, "invalid argument to user-defined notation, must be closed term"); } parser = mk_app(parser, e);