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

fix(frontends/lean/decl_cmds): do not allow section parameters/variables to shadow existing parameters/variables

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-02 18:29:41 -07:00
parent a52b21c92d
commit 6950b4aa9b
3 changed files with 14 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/decl_cmds.cpp
View file

@ -85,6 +85,8 @@ static environment declare_var(parser & p, environment env,
lean_assert(k == variable_kind::Parameter || k == variable_kind::Variable); lean_assert(k == variable_kind::Parameter || k == variable_kind::Variable);
if (k == variable_kind::Parameter) if (k == variable_kind::Parameter)
check_parameter_type(p, n, type, pos); check_parameter_type(p, n, type, pos);
if (p.get_local(n))
throw parser_error(sstream() << "invalid declaration, section/context already contains '" << n << "'", pos);
name u = p.mk_fresh_name(); name u = p.mk_fresh_name();
expr l = p.save_pos(mk_local(u, n, type, bi), pos); expr l = p.save_pos(mk_local(u, n, type, bi), pos);
p.add_local_expr(n, l, k == variable_kind::Variable); p.add_local_expr(n, l, k == variable_kind::Variable);

11
tests/lean/sec.lean Normal file
View file

@ -0,0 +1,11 @@
import data.prod
open prod
section
variable A : Type
variable a : A
variable A : Type
variable b : A
definition foo := a
end

1
tests/lean/sec.lean.expected.out Normal file
View file

@ -0,0 +1 @@
sec.lean:7:11: error: invalid declaration, section/context already contains 'A'