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

fix(frontends/lean/vm_elaborator): initialization

Browse source
This commit is contained in:
Sebastian Ullrich 2019-01-17 13:34:28 +01:00
parent 0923a2cbae
commit 15cc07fe17
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/vm_elaborator.cpp
View file

@ -34,7 +34,7 @@ namespace lean {
struct resolve_names_fn : public replace_visitor {
parser & m_p;
names m_locals;
bool m_assume_local;
bool m_assume_local = false;
resolve_names_fn(parser & p) : m_p(p) {}