<div dir="ltr">Not really, it's not my area of expertise. Maybe someone else on the list can help. Cheers, -- P<div><br clear="all"><div><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div><div dir="ltr"><br></div><div>Too brief? Here's why: <a href="http://www.emailcharter.org/" target="_blank">http://www.emailcharter.org/</a></div></div></div></div></div></div><br></div></div><br><div class="gmail_quote"><div dir="ltr">On Mon, 19 Nov 2018 at 18:44, Marko Dimjašević <<a href="mailto:marko@dimjasevic.net">marko@dimjasevic.net</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Dear Philip,<br>
<br>
On Mon, 2018-11-19 at 08:55 +0000, Philip Wadler wrote:<br>
> <br>
> I find this ability useful. However, an attempt to normalise a term<br>
> that depends on a postulate will yield a term in which the postulate<br>
> appears rather than raising an error. It would be helpful if Agda had<br>
> an option to raise an error in such circumstances, and to indicate in<br>
> a file terms to be normalised to confirm they don't depend on such<br>
> postulates. <br>
<br>
<br>
Thank you for your reply. What you wrote sounds related to typed<br>
holes. <br>
<br>
Is there a particular resource you would recommend for learning about<br>
normalisation?<br>
<br>
<br>
Kind regards,<br>
Marko Dimjašević<br>
</blockquote></div>