ckrause
ckrause
```asm ; A094186: lpb $0 sub $0,2 mov $1,0 lpb $0 add $1,1 sub $0,$1 lpe lpe ; A002262: lpb $0 add $1,1 sub $0,$1 lpe ```
Folded program: ```asm lpb $0 sub $0,2 mov $1,0 seq $0,2262 lpe ```
``` libc++abi: terminating due to uncaught exception of type std::runtime_error: seq using negative argument: 2262 Abort trap: 6 ```
added comparison operators
That's great. I still want to keep this issue open though, because it shows that the the incremental evaluation and the formula generation could be generalized, which could be useful...
Internal work for mining user-defined seqs has been done already, but the feature is not available in v25.8.24 yet. Will be probably included in the next release.
@copilot The max number of initial terms should remain at 10. We should continue to reject this program. However, it would be great if the formula generation could fail fast...
@copilot Revert the additional check for intial terms. Instead, impose stronger limits in `simplifyFormulaUsingVariants()` to reduce the execessive runtime of the formula generation for A000033.
@copilot Can you use [Nat.nthRoot](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/NthRoot/Defs.html#Nat.nthRoot) instead of creating a helper function? Please also add formula tests.
For non-negative arguments (`Nat`), we could use [Nat.choose](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Choose/Basic.html#Nat.choose). But then we would need to integrate a range check to find out if it is non-negative.