[Agda] Solving Presburger arithmetic goals

[Rodrigo Ribeiro]

Hi!

I'm trying to prove the correctness of an algorithm and I'm facing some
boring proofs that could be easily proved (in Coq, at least...) by a
decision procedure for the Presburger arithmetic.

I noticed that the Standard library has solvers for semi-rings. Is there
some solver for Presburger arithmetic ?

-- Rodrigo
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130909/af978e11/attachment.html