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

chore(kernel): remove dead code, we don't have level constraints anymore

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-21 15:46:17 -07:00
parent b9d7f8e867
commit a45dc0bb86
3 changed files with 0 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/kernel/error_msgs.cpp
View file

@ -41,12 +41,4 @@ format pp_def_type_mismatch(formatter const & fmt, environment const & env, opti
r += pp_indent_expr(fmt, env, opts, given_type);
return r;
}
format pp_def_lvl_cnstrs_satisfied(formatter const & fmt, environment const & env, options const & opts, expr const & e,
level const & lhs, level const & rhs) {
format r("constand definition level constraints are not satisfied");
r += pp_indent_expr(fmt, env, opts, e);
r += format("level constraint:");
r += pp(lhs, rhs, opts);
return r;
}
}

2
src/kernel/error_msgs.h
View file

@ -15,6 +15,4 @@ format pp_app_type_mismatch(formatter const & fmt, environment const & env, opti
expr const & expected_type, expr const & given_type);
format pp_def_type_mismatch(formatter const & fmt, environment const & env, options const & opts, name const & n,
expr const & expected_type, expr const & given_type);
format pp_def_lvl_cnstrs_satisfied(formatter const & fmt, environment const & env, options const & opts, expr const & e,
level const & lhs, level const & rhs);
}

12
src/kernel/type_checker.cpp
View file

@ -219,18 +219,6 @@ struct type_checker::imp {
}
}
/** \brief Create a justification for the level constraint <tt>lhs <= rhs</tt> associated with constanc \c c. */
justification mk_lvl_cnstr_jst(expr const & c, level const & lhs, level const & rhs) {
lean_assert(is_constant(c));
return mk_justification(c,
[=](formatter const & fmt, options const & o, substitution const & subst) {
return pp_def_lvl_cnstrs_satisfied(fmt, m_env, o,
subst.instantiate_metavars_wo_jst(c),
subst.instantiate_metavars_wo_jst(lhs),
subst.instantiate_metavars_wo_jst(rhs));
});
}
/**
\brief Create a justification for a application type mismatch,
\c e is the application, \c fn_type and \c arg_type are the function and argument type.