let linear_combination
subsume ring
#11990
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 seems like it would be perfectly coherent to let
linear_combination
with no arguments be an alias forring
-- in fact, this is arguably the correct behaviour for that input, rather than (as currently) failing.See https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F.20tactics/topic/trivial.20case.20of.20linear_combination for discussion. @robertylewis says
The text was updated successfully, but these errors were encountered: