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

feat(kernel/justification): add function for creating simple justification objects

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-15 11:16:48 -07:00
parent d58b8a8102
commit 830537a58b
2 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/kernel/justification.cpp
View file

@ -241,7 +241,12 @@ justification mk_justification(optional<expr> const & s, pp_jst_sfn const & fn)
return mk_justification(s, [=](formatter const & fmt, options const & opts, pos_info_provider const * p, substitution const & subst) {
return compose(to_pos(s, p), fn(fmt, opts, subst)); });
}
justification mk_justification(char const * msg, optional<expr> const & s) {
std::string _msg(msg);
return mk_justification(s, [=](formatter const &, options const &, pos_info_provider const *, substitution const &) {
return format(_msg);
});
}
std::ostream & operator<<(std::ostream & out, justification const & j) {
if (j.is_none()) {
out << "none";

1
src/kernel/justification.h
View file

@ -110,6 +110,7 @@ justification mk_assumption_justification(unsigned idx);
\brief Create a justification for constraints produced by the type checker.
*/
justification mk_justification(optional<expr> const & s, pp_jst_fn const & fn);
justification mk_justification(char const * msg, optional<expr> const & s = none_expr());
/**
\brief Create a justification for constraints produced by the type checker.
It is similar to the previous function, but the position of \c s will be automatically included.