[Agda] Data.Rational

[Noam Zeilberger]

When I was programming with rationals in Agda, I also found the approach of
maintaining coprime proofs intractable, especially since I wanted the
typechecker to perform actual arithmetic and it was expensive to compute
these proofs.  I ended up settling on a purely axiomatic approach,
including a patch to Agda to support BUILTIN RATIONAL.

On Tue, Mar 11, 2014 at 11:43 AM, Li Nuo <gabrno at gmail.com> wrote:

> Hi,
>
> I think you can use an alternative approach to make the definition
> simpler. You could define the setoid version (namely fractions which
> doesn't have to be reduced) and use what we call "definable quotient
> structure" to relate the setoid definition with the normal form definition
> (which you can find here
> http://www.cs.nott.ac.uk/~txa/publ/defquotients.pdf).
>

Incidentally, have you tried to relate this notion to Cyril Cohen's work on
"pragmatic" quotient types in Coq (see
http://perso.crans.org/cohen/work/quotients/)?

Noam
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140311/c928047c/attachment.html