Commit 2023-03-09 14:54 46137576

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.