Consider implementing number literals

[dcz-self]

Peano arithmetics is cool, but entering chains of s(s(... is impractical.
Numbers could be reparsed as those chains, but it makes me worry about the depth of the AST in my use case (counting potentially to a few millions).

I tried to hack in a solution, but I haven't found a way to supply predicates like % / etc. after parsing the literal.

What would be the best way to do that? Create a separate term containing the number that is not applicative?

[fatho]

Peano arithmetics is cool, but entering chains of s(s(... is impractical.

Agreed, that's more of a toy than a really usable arithmetic implementation.

What would be the best way to do that? Create a separate term containing the number that is not applicative?

Indeed, a new term type would be the way to go I think.

Defining custom predicates is more complicated. I tried something in this branch https://github.com/fatho/logru/compare/more-builtins but it still feels a bit chaotic due to how the solver interacts with different types of "universes".

Since this is more of a hobby project to me, I won't really have a lot of time expanding this. But feel free to take that branch as a base.

[fatho]

Had some time to work a bit on this project after all. I think this can be considered done after #18, and with cut implemented (#20), it should be possible to build some useful high-level abstractions on top of that.

[dcz-self]

Thanks for implementing so much stuff!