[Agda] An error function and totality

[Philip Wadler]

Not really, it's not my area of expertise. Maybe someone else on the list
can help. Cheers, -- P

.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

Too brief? Here's why: http://www.emailcharter.org/


On Mon, 19 Nov 2018 at 18:44, Marko Dimjašević <marko at dimjasevic.net> wrote:

> Dear Philip,
>
> On Mon, 2018-11-19 at 08:55 +0000, Philip Wadler wrote:
> >
> > I find this ability useful. However, an attempt to normalise a term
> > that depends on a postulate will yield a term in which the postulate
> > appears rather than raising an error. It would be helpful if Agda had
> > an option to raise an error in such circumstances, and to indicate in
> > a file terms to be normalised to confirm they don't depend on such
> > postulates.
>
>
> Thank you for your reply. What you wrote sounds related to typed
> holes.
>
> Is there a particular resource you would recommend for learning about
> normalisation?
>
>
> Kind regards,
> Marko Dimjašević
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181119/a20493c3/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181119/a20493c3/attachment.ksh>