Commit 2022-12-16 09:48 ddf4802e

perf: improve to_additive performance (#1060) Using

def Ones : ℕ → Q(Nat)
| 0     => q(1)
| (n+1) => q($(Ones n) + $(Ones n))

The new to_additive takes 45ms on Ones 500 (higher gives stack overflows) The old to_additive takes 13794ms on Ones 17 (exponential in the argument) There is still one issue workaround by using transform in etaExpand.

• Remove replaceRecM and replaceRecMeta that are exponentially slow
• Remove replaceRecTraversal because its interface is less convenient than replaceRec