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

fix(frontends/lean/structure_cmd): make sure structure_cmd takes the option default_priority into account

Browse source
This commit is contained in:
Leonardo de Moura 2016-10-01 13:47:19 -07:00
parent 9631b70295
commit 4f69fe943a
2 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/frontends/lean/decl_attributes.h
View file

@ -10,6 +10,7 @@ Author: Leonardo de Moura
#include "library/attribute_manager.h"
#include "library/io_state.h"
namespace lean {
unsigned get_default_priority(options const & opts);
class parser;
class decl_attributes {
public:

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

@ -104,6 +104,7 @@ struct structure_cmd_fn {
bool m_inductive_predicate;
levels m_ctx_levels; // context levels for creating aliases
buffer<expr> m_ctx_locals; // context local constants for creating aliases
unsigned m_prio;
structure_cmd_fn(parser & p, decl_attributes const & attrs, decl_modifiers const & modifiers):
m_p(p),
@ -115,6 +116,7 @@ struct structure_cmd_fn {
m_explicit_universe_params = false;
m_infer_result_universe = false;
m_inductive_predicate = false;
m_prio = get_default_priority(p.get_options());
}
void check_attrs(decl_attributes const & attrs, pos_info const & pos) const {
@ -817,7 +819,7 @@ struct structure_cmd_fn {
if (!m_private_parents[i]) {
if (m_attrs.has_class() && is_class(m_env, parent_name)) {
// if both are classes, then we also mark coercion_name as an instance
m_env = add_instance(m_env, coercion_name, LEAN_DEFAULT_PRIORITY, true);
m_env = add_instance(m_env, coercion_name, m_prio, true);
}
}
}