extend syntax for filter_upwards
#11616
Labels
feature-request
This issue is a feature request, either for mathematics, tactics, or CI
modifies-tactic-syntax
This PR adds a new interactive tactic or modifies the syntax of an existing tactic.
t-meta
Tactics, attributes or user commands
It'd be nice to
(1) implement syntax
filter_upwards [...] with x h1 h2
for the currentfilter_upwards [...], intros x h1 h2
(2) change the current syntax
filter_upwards [...] a
tofilter_upwards [...] using a
https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F.20tactics/topic/filter_upwards
The text was updated successfully, but these errors were encountered: