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

fix(kernel/formatter): fixes #21

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-01 15:07:01 -07:00
parent bd766d8b0e
commit 288831dc66
1 changed files with 11 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/kernel/formatter.cpp
View file

@ -31,9 +31,19 @@ name pick_unused_name(expr const & t, name const & s) {
return r; return r;
} }
bool is_internal_name(name n) {
while (!n.is_atomic())
n = n.get_prefix();
return n.is_numeral();
}
static name g_x("x");
std::pair<expr, expr> binding_body_fresh(expr const & b, bool preserve_type) { std::pair<expr, expr> binding_body_fresh(expr const & b, bool preserve_type) {
lean_assert(is_binding(b)); lean_assert(is_binding(b));
name n = pick_unused_name(binding_body(b), binding_name(b)); name n = binding_name(b);
if (is_internal_name(n))
n = g_x;
n = pick_unused_name(binding_body(b), n);
expr c = mk_local(n, preserve_type ? binding_domain(b) : expr()); expr c = mk_local(n, preserve_type ? binding_domain(b) : expr());
return mk_pair(instantiate(binding_body(b), c), c); return mk_pair(instantiate(binding_body(b), c), c);
} }