Leonardo de Moura 1c6e70d170 feat(library/init/meta): introv tactic ... @Armael: this commit implements the `introv` tactic. The implementation uses an auxiliary `intros_dep` that introduces new hypotheses with forward dependencies. The `tactic.introv` tactic implemented at library/init/meta/tactic.lean is the main implementation, but it is not nice for interactive use since users would have to write ``` tactic.introv [`h1, `h2] ``` To make it more conveninent to use, we define another ``` meta def introv (ns : parse ident_*) : tactic unit := tactic.introv ns >> return () ``` This one is in the namespace `tactic.interactive`, and uses parser extensions. The argument `parse ident_*` instructs the parser to parse 0 or more identifiers and create a term of type `list name` containing these identifiers.		2017-05-31 14:09:25 -07:00
..
lean	feat(library/init/meta): introv tactic	2017-05-31 14:09:25 -07:00
.gitignore	chore(tests/lean,shell/lean): run leantests and leanruntests in parallel	2017-03-30 06:04:00 +02:00