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

fix(frontends/lean/elaborator): fix try_monad_coercion

Browse source
This commit is contained in:
Sebastian Ullrich 2018-10-02 13:08:25 -07:00
parent 918388ac26
commit 25b9deab15
2 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/frontends/lean/elaborator.cpp
View file

@ -662,7 +662,7 @@ bool elaborator::is_monad_fail(expr const & e) {
tactic ?a ===> smt_tactic unit
TODO(leo): can/should we generalize this approach? */
optional<expr> elaborator::try_monad_coercion(expr const & e, expr const & e_type, expr type, expr const & ref) {
optional<expr> elaborator::try_monad_coercion(expr const & e, expr e_type, expr type, expr const & ref) {
if ((has_expr_metavar(e_type) && has_expr_metavar(type))
|| (!has_expr_metavar(e_type) && !has_expr_metavar(type))
|| !is_app(e_type)
@ -677,6 +677,7 @@ optional<expr> elaborator::try_monad_coercion(expr const & e, expr const & e_typ
}
if (!m_ctx.is_def_eq(app_arg(e_type), app_arg(type)))
return none_expr();
e_type = instantiate_mvars(e_type);
type = instantiate_mvars(type);
return mk_coercion_core(e, e_type, type, ref);
}

2
src/frontends/lean/elaborator.h
View file

@ -138,7 +138,7 @@ private:
optional<expr> mk_coercion_core(expr const & e, expr const & e_type, expr const & type, expr const & ref);
bool is_monad(expr const & e);
bool is_monad_fail(expr const & e);
optional<expr> try_monad_coercion(expr const & e, expr const & e_type, expr type, expr const & ref);
optional<expr> try_monad_coercion(expr const & e, expr e_type, expr type, expr const & ref);
optional<expr> mk_coercion(expr const & e, expr e_type, expr type, expr const & ref);
void trace_coercion_fn_sort_failure(bool is_fn, expr const & e_type, expr const & ref, char const * error_msg);