54004d4972
The `induction h` tactic tries to clear hypothesis `h` after it is applied. But, before this commit, `cases h` would only try to clear `h` when performing non-dependent elimination. This was problematic when writing tactic scripts for automating proofs.
21 lines
588 B
Text
21 lines
588 B
Text
universes u v
|
||
|
||
inductive tree (α : Type u)
|
||
| leaf {} : tree
|
||
| node (l : tree) (v : α) (r : tree) : tree
|
||
|
||
namespace tree
|
||
variables {α : Type u}
|
||
|
||
inductive is_searchable (lt : α → α → Prop) : tree α → α → α → Prop
|
||
| leaf_s {lo hi} : lt lo hi → is_searchable leaf lo hi
|
||
| node_s {l r v lo hi} (hs₁ : is_searchable l lo v) (hs₂ : is_searchable r v hi) : is_searchable (node l v r) lo hi
|
||
|
||
example (l r : tree α) {lo v hi lt} (h : is_searchable lt (node l v r) lo hi) : true :=
|
||
begin
|
||
cases h,
|
||
trace_state, /- Should not contain h -/
|
||
trivial
|
||
end
|
||
|
||
end tree
|