fix(library/tactic/exact_tactic): fixes #779
This commit is contained in:
parent
f21647899f
commit
6a079fdd2d
3 changed files with 7 additions and 1 deletions
|
@ -34,7 +34,7 @@ tactic exact_tactic(elaborate_fn const & elab, expr const & e, bool enforce_type
|
|||
return none_proof_state();
|
||||
}
|
||||
expr t = head(gs).get_type();
|
||||
bool report_unassigned = !allow_metavars && enforce_type_during_elaboration;
|
||||
bool report_unassigned = !allow_metavars && enforce_type_during_elaboration && s.report_failure();
|
||||
optional<expr> new_e;
|
||||
try {
|
||||
new_e = elaborate_with_respect_to(env, ios, elab, new_s, e, some_expr(t),
|
||||
|
|
4
tests/lean/779.hlean
Normal file
4
tests/lean/779.hlean
Normal file
|
@ -0,0 +1,4 @@
|
|||
definition foo (x : empty) : empty :=
|
||||
by try exact _;contradiction
|
||||
|
||||
print foo
|
2
tests/lean/779.hlean.expected.out
Normal file
2
tests/lean/779.hlean.expected.out
Normal file
|
@ -0,0 +1,2 @@
|
|||
definition foo : empty → empty :=
|
||||
empty.rec (λ (e : empty), empty)
|
Loading…
Reference in a new issue