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

feat(frontends/lean/server): use '?a' instead of '?M_i' for implicit arguments when displaying FINDP and FINDG matches

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-09-07 09:36:03 -07:00
parent 1bc31d7df0
commit 6d2df80a17
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/frontends/lean/server.cpp
View file

@ -498,13 +498,14 @@ void server::display_decl(name const & short_name, name const & long_name, envir
io_state_stream out = regular(env, m_ios).update_options(o);
expr type = d.get_type();
if (LEAN_FIND_CONSUME_IMPLICIT) {
name_generator ngen("M");
while (true) {
if (!is_pi(type))
break;
if (!binding_info(type).is_implicit())
break;
expr m = mk_metavar(ngen.next(), binding_domain(type));
std::string q("?");
q += binding_name(type).to_string();
expr m = mk_constant(name(q.c_str()));
type = instantiate(binding_body(type), m);
}
}