diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 06456a4c23..535f40fc13 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -3510,8 +3510,7 @@ expr elaborator::visit_suffices_expr(expr const & e, optional const & expe } static expr mk_emptyc(expr const & src) { - return copy_pos(src, mk_app(copy_pos(src, mk_constant(get_has_emptyc_emptyc_name())), - copy_pos(src, mk_expr_placeholder()))); + return copy_pos(src, mk_constant(get_has_emptyc_emptyc_name())); } expr elaborator::visit_emptyc_or_emptys(expr const & e, optional const & expected_type) { diff --git a/src/frontends/lean/inductive_cmds.cpp b/src/frontends/lean/inductive_cmds.cpp index 863157a613..2563c85251 100644 --- a/src/frontends/lean/inductive_cmds.cpp +++ b/src/frontends/lean/inductive_cmds.cpp @@ -125,7 +125,7 @@ struct inductive_cmd_fn { if (auto it = m_implicit_infer_map.find(n)) return *it; else - return implicit_infer_kind::Implicit; + return implicit_infer_kind::RelaxedImplicit; } /** \brief Return true if eliminator/recursor can eliminate into any universe */ @@ -384,7 +384,7 @@ struct inductive_cmd_fn { ir_name = get_namespace(m_env) + ir_name; parser::local_scope S(m_p); buffer params; - implicit_infer_kind kind = implicit_infer_kind::Implicit; + implicit_infer_kind kind = implicit_infer_kind::RelaxedImplicit; m_p.parse_optional_binders(params, kind); m_implicit_infer_map.insert(ir_name, kind); for (expr const & param : params) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index e14d52244b..02a40f7e55 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -869,11 +869,11 @@ void parser::parse_binders_core(buffer & r, parse_binders_config & cfg) { /* Parse {} prefix */ if (is_implicit(*bi) && curr_is_token(get_rcurly_tk())) { next(); - *cfg.m_infer_kind = implicit_infer_kind::RelaxedImplicit; + *cfg.m_infer_kind = implicit_infer_kind::Implicit; first = false; continue; } else { - *cfg.m_infer_kind = implicit_infer_kind::Implicit; + *cfg.m_infer_kind = implicit_infer_kind::RelaxedImplicit; } } unsigned rbp = 0; diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 6630fd1002..7d3c4ab7a6 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -156,8 +156,8 @@ struct parser : public abstract_parser { If m_infer_kind != nullptr, then a sequence of binders can be prefixed with '{}' Moreover, *m_infer_kind will be updated with - - implicit_infer_kind::RelaxedImplicit if prefix is '{}' - - implicit_infer_kind::Implicit, otherwise. */ + - implicit_infer_kind::Implicit if prefix is '{}' + - implicit_infer_kind::RelaxedImplicit, otherwise. */ implicit_infer_kind * m_infer_kind{nullptr}; /* (output) It is set to true if the last binder is surrounded with some kind of bracket (e.g., '()', '{}', '[]'). */ diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index feb8725dc3..61b0e6e4a0 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -227,7 +227,7 @@ struct structure_cmd_fn { bool m_has_new_default; // if true, (re-)declare default value in this structure field_decl(expr const & local, optional const & default_val, field_kind kind, - implicit_infer_kind infer_kind = implicit_infer_kind::Implicit): + implicit_infer_kind infer_kind = implicit_infer_kind::RelaxedImplicit): m_local(local), m_default_val(default_val), m_kind(kind), m_infer_kind(infer_kind), m_has_new_default(default_val && kind == field_kind::new_field) {} @@ -783,7 +783,7 @@ struct structure_cmd_fn { expr type; expr default_value; bool default_value_initialized = false; - implicit_infer_kind kind = implicit_infer_kind::Implicit; + implicit_infer_kind kind = implicit_infer_kind::RelaxedImplicit; { parser::local_scope scope(m_p); buffer params; @@ -1065,7 +1065,7 @@ struct structure_cmd_fn { if (!m_subobjects || field.m_kind != field_kind::from_parent) { proj_names.push_back(m_name + local_name_p(field.m_local)); infer_kinds.push_back( - field.m_infer_kind != implicit_infer_kind::Implicit ? field.m_infer_kind : m_mk_infer); + field.m_infer_kind != implicit_infer_kind::RelaxedImplicit ? field.m_infer_kind : m_mk_infer); } } m_env = mk_projections(m_env, m_name, proj_names, infer_kinds, m_meta_info.m_attrs.has_class()); @@ -1277,7 +1277,7 @@ struct structure_cmd_fn { if (m_p.curr_is_token(get_lparen_tk()) || m_p.curr_is_token(get_lcurly_tk()) || m_p.curr_is_token(get_lbracket_tk())) { m_mk_short = LEAN_DEFAULT_STRUCTURE_INTRO; - m_mk_infer = implicit_infer_kind::Implicit; + m_mk_infer = implicit_infer_kind::RelaxedImplicit; } else { m_mk_short = m_p.check_atomic_id_next("invalid 'structure', atomic identifier expected"); m_mk_infer = parse_implicit_infer_modifier(m_p); @@ -1289,7 +1289,7 @@ struct structure_cmd_fn { } else { m_mk_pos = m_name_pos; m_mk_short = LEAN_DEFAULT_STRUCTURE_INTRO; - m_mk_infer = implicit_infer_kind::Implicit; + m_mk_infer = implicit_infer_kind::RelaxedImplicit; m_mk = m_name + m_mk_short; process_empty_new_fields(); } diff --git a/src/frontends/lean/type_util.cpp b/src/frontends/lean/type_util.cpp index 243852d36f..0343fa9705 100644 --- a/src/frontends/lean/type_util.cpp +++ b/src/frontends/lean/type_util.cpp @@ -36,9 +36,9 @@ implicit_infer_kind parse_implicit_infer_modifier(parser & p) { if (p.curr_is_token(get_lcurly_tk())) { p.next(); p.check_token_next(get_rcurly_tk(), "invalid introduction rule, '}' expected"); - return implicit_infer_kind::RelaxedImplicit; - } else { return implicit_infer_kind::Implicit; + } else { + return implicit_infer_kind::RelaxedImplicit; } } }