Remainder operation is disabled

leoprover / Leo-III

An Automated Theorem Prover for Classical Higher-Order Logic with Henkin Semantics

http://inf.fu-berlin.de/~lex/leo3

BSD 3-Clause "New" or "Revised" License

41 stars 10 forks source link

Remainder operation is disabled #76

Open gistya opened 5 months ago

gistya commented 5 months ago

In trying to use LEO, I ran into the issue that the remainder operations $remainder_t, $remainder_e are commented out in the current code. Are these operations simply not supported or is there something I need to do in order to activate them? Thanks.

https://github.com/leoprover/Leo-III/blob/029813a871bed771116dc44744bf3d2628914bac/src/main/scala/leo/modules/HOLSignature.scala#L464

lex-lex commented 5 months ago

Hi, I'm sorry to say that these operations are currently not supported in Leo-III. We're working on support for arithmetic at the moment, but it's unclear how fast (and how comprehensive) this will be.