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

fix(frontends/lean/tactic_evaluator): 'begin [smt] ... end' block nested in regular one

Browse source
This commit is contained in:
Leonardo de Moura 2017-01-07 13:12:51 -08:00
parent 8069872861
commit 299751982b
2 changed files with 5 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/tactic_evaluator.cpp
View file

@ -151,7 +151,7 @@ tactic_state tactic_evaluator::execute_begin_end(tactic_state const & s, buffer<
get_begin_end_block_elements(tactic, nested_tactics);
new_s = execute_begin_end(new_s, nested_tactics, curr_ref);
} else if (is_smt_begin_end_block(tactic)) {
new_s = execute_smt_begin_end(s, tactic, ref);
new_s = execute_smt_begin_end(new_s, tactic, curr_ref);
} else {
throw elaborator_exception(curr_ref, "ill-formed 'begin ... end' tactic block");
}

11
tests/lean/smt_begin_end1.lean.expected.out
View file

@ -5,10 +5,7 @@ h : p (f a) (f a)
facts: {p (f a) (f a), p (f a) (f b), a = b}
equalities: {{b, a}, {f a, f b}}
⊢ p a b
a b c : ℕ,
a_1 : a = b,
a_2 : p (f a) (f b),
h₁ : p (f a) (f a)
facts: {p (f a) (f a), p (f a) (f b), a = b}
equalities: {{b, a}, {f a, f b}}
⊢ p a b
a c : ℕ,
a_1 h₁ : p (f a) (f a)
facts: {p (f a) (f a)}
⊢ p a a