Commit 2022-11-24 01:53 822c8702

fix: fix to_additive handling of Nat and Int (#689)

• Remove [to_additive] attributes from Nat and Int. That attribute disables all useful heuristics for to_additive on these types.
• deal with literals in specific types, like Nat. This uses a new attribute @[to_additive_fixed_numeral].
• Add to_additive_relevant_arg attribute for heterogenous operations
• Fix to_additive_reorder arguments on HPow.hPow
• Fix parsing of to_additive_relevant_arg to use 1-indexed numbers instead of 0-indexed numbers
• Do not add relevantArgAttr on many declarations if they would have the default value anyway.
• Revert test foo2 in tests/ToAdditive to the Lean 3 behavior. Previosuly the test would only succeed if the heuristics for Nat and Int were disabled.
• Some cleanup in code, comments and docs