Commit 2023-03-09 14:54 46137576
View on Github →Fix: to_additive doesn't translate numeral literals by default (#2726)
- The numeral literal 1 only gets replaced by 0 in a few whitelisted declarations
- The previous behavior was to replace the numeral 1 by the numeral 0 always, unless it occurs in a list of blacklisted declarations. However,
norm_num
and other tactics give proofs with many numeral literals in many different declarations, and these literals - I believe - always represent natural numbers. Therefore, we had to blacklist very many declarations. The new default improves the situation.