max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(frontends/lean/decl_util): truly fix top-level do pattern names race

Browse source
This commit is contained in:
Sebastian Ullrich 2017-03-29 14:16:34 +02:00 • committed by Gabriel Ebner
parent ef5cf54a86
commit 7a147eab12
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -357,7 +357,7 @@ environment add_alias(environment const & env, bool is_protected, name const & c
struct definition_info {
name m_prefix;
bool m_is_private{false};
bool m_is_private{true}; // pattern matching outside of definitions should generate private names
bool m_is_meta{false};
bool m_is_noncomputable{false};
bool m_is_lemma{false};