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

fix(library/eval_helper): evaluating tactics

Browse source
This commit is contained in:
Sebastian Ullrich 2017-05-31 16:07:08 +02:00
parent f820f3f97e
commit 834375a042
3 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/eval_helper.cpp
View file

@ -67,7 +67,7 @@ optional<vm_obj> eval_helper::try_exec_io() {
optional<vm_obj> eval_helper::try_exec_tac() {
if (is_constant(get_app_fn(m_ty), get_tactic_name())) {
auto tac_st = mk_tactic_state_for(m_env, m_opts, m_fn, m_tc.mctx(), m_tc.lctx(), mk_true());
m_vms.push(tactic::to_obj(tac_st));
m_args.push_back(tactic::to_obj(tac_st));
auto r = invoke_fn();
if (tactic::is_result_success(r)) {
return optional<vm_obj>(tactic::get_result_value(r));

2
tests/lean/eval_tactic.lean Normal file
View file

@ -0,0 +1,2 @@
#eval tactic.trace 42
#eval (tactic.fail "nope" : tactic nat)

2
tests/lean/eval_tactic.lean.expected.out Normal file
View file

@ -0,0 +1,2 @@
42
eval_tactic.lean:2:0: error: nope