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

fix(frontends/lean/migrate_cmd): bug when using migrate command with option --to_axiom

Browse source
This commit is contained in:
Leonardo de Moura 2015-03-30 16:20:02 -07:00
parent 3132d229c0
commit 46777fdd1d
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/frontends/lean/migrate_cmd.cpp
View file

@ -204,7 +204,9 @@ struct migrate_cmd_fn {
expr new_type = Pi(m_params, t); expr new_type = Pi(m_params, t);
expr new_value = Fun(m_params, v); expr new_value = Fun(m_params, v);
try { try {
if (d.is_theorem()) if (d.is_axiom())
m_env = module::add(m_env, check(m_env, mk_theorem(full_name, ls, new_type, new_value)));
else if (d.is_theorem())
m_env = module::add(m_env, check(m_env, mk_theorem(full_name, ls, new_type, new_value))); m_env = module::add(m_env, check(m_env, mk_theorem(full_name, ls, new_type, new_value)));
else else
m_env = module::add(m_env, check(m_env, mk_definition(m_env, full_name, ls, m_env = module::add(m_env, check(m_env, mk_definition(m_env, full_name, ls,
@ -414,7 +416,7 @@ struct migrate_cmd_fn {
environment env = m_env; environment env = m_env;
env.for_each_declaration([&](declaration const & d) { env.for_each_declaration([&](declaration const & d) {
if (!d.is_definition() && !d.is_theorem()) if (!d.is_definition() && !d.is_theorem() && !d.is_axiom())
return; return;
if (std::find(m_hiding.begin(), m_hiding.end(), d.get_name()) != m_hiding.end()) if (std::find(m_hiding.begin(), m_hiding.end(), d.get_name()) != m_hiding.end())
return; return;