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

feat(library/init/meta/interactive): add match_target pat interactive tactic

Browse source
This commit is contained in:
Leonardo de Moura 2017-12-05 12:25:17 -08:00
parent b1e8270172
commit 6f943d77a2
1 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
library/init/meta/interactive.lean
View file

@ -6,7 +6,7 @@ Authors: Leonardo de Moura
prelude
import init.meta.tactic init.meta.rewrite_tactic init.meta.simp_tactic
import init.meta.smt.congruence_closure init.category.combinators
import init.meta.interactive_base init.meta.derive
import init.meta.interactive_base init.meta.derive init.meta.match_tactic
open lean
open lean.parser
@ -1205,6 +1205,12 @@ We use this tactic for writing tests.
meta def guard_hyp (n : parse ident) (p : parse $ tk ":=" *> texpr) : tactic unit :=
do h ← get_local n >>= infer_type, guard_expr_eq h p
/--
`match_target t` fails if target does not match pattern `t`.
-/
meta def match_target (t : parse texpr) : tactic unit :=
tactic.match_target t >> skip
/--
`by_cases p with h` splits the main goal into two cases, assuming `h : p` in the first branch, and `h : ¬ p` in the second branch.