From db08f3f13936ea2703ace230b66a7d78bca620e1 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 2 Jun 2017 13:39:50 +0200 Subject: [PATCH] fix(frontends/lean/user_notation): check for closedness before evaluating term --- src/frontends/lean/user_notation.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/frontends/lean/user_notation.cpp b/src/frontends/lean/user_notation.cpp index 76e5ccead0..bd4c60a14c 100644 --- a/src/frontends/lean/user_notation.cpp +++ b/src/frontends/lean/user_notation.cpp @@ -59,7 +59,11 @@ static environment add_user_notation(environment const & env, name const & d, un if (is_app_of(arg_type, get_interactive_parse_name())) { parser = mk_app(parser, parse_interactive_param(p, arg_type)); } else { - parser = mk_app(parser, p.parse_expr(get_max_prec())); + expr e = p.parse_expr(get_max_prec()); + if (!closed(e) || has_local(e)) { + throw elaborator_exception(e, "invalid argument to user-defined notation, must be closed term"); + } + parser = mk_app(parser, e); } } parser = p.elaborate("_user_notation", {}, parser).first;