Leonardo de Moura 56dba5b98a fix(frontends/lean/elaborator): fixes #1930 ... @kha the following idiom is not safe ``` while (is_pi(t)) { t = whnf(binding_body(t)); } ``` `whnf(e)` assumes that `e` does not have dangling deBruijn variables. We should use (the more expensive): ``` while (is_pi(t)) { t = whnf(instantiate(binding_body(t), locals.push_local_from_binding(t))); } ``` BTW, this problem is not related to the assertion violation at #1930 I just stumbled on it when fixing the violation.		2018-02-19 08:51:26 -08:00
..
lean	fix(frontends/lean/elaborator): fixes #1930	2018-02-19 08:51:26 -08:00
.gitignore	chore(tests/lean,shell/lean): run leantests and leanruntests in parallel	2017-03-30 06:04:00 +02:00