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

fix(frontends/lean/structure_cmd): generate code for automatically generated coercions

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-08 13:58:34 -07:00
parent 1d6b1d381b
commit 53aa89f1e1
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/structure_cmd.cpp
View file

@ -39,6 +39,7 @@ Author: Leonardo de Moura
#include "library/kernel_serializer.h"
#include "library/type_context.h"
#include "library/app_builder.h"
#include "library/compiler/vm_compiler.h"
#include "library/definitional/rec_on.h"
#include "library/definitional/induction_on.h"
#include "library/definitional/cases_on.h"
@ -845,6 +846,7 @@ struct structure_cmd_fn {
m_env = set_reducible(m_env, coercion_name, reducible_status::Reducible, true);
save_def_info(coercion_name);
add_alias(coercion_name);
m_env = vm_compile(m_env, m_env.get(coercion_name));
if (!m_private_parents[i]) {
// if (!m_modifiers.is_class() || !is_class(m_env, parent_name))
// m_env = add_coercion(m_env, m_p.ios(), coercion_name, true);