<div dir="ltr">Thanks, Martin. So which fragment do you recommend? Cheers, -- P</div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature" data-smartmail="gmail_signature"><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></div></div>
<br><div class="gmail_quote">On 16 May 2018 at 16:03, Martin Escardo <span dir="ltr"><<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class=""><br>
<br>
On 16/05/18 20:37, Philip Wadler wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Thanks for following up. It is the latter case. But I don't understand why it should be ok for that to fail. Removing abstract should just replace some abstract terms by their concretions, which have already been type checked. Everything that was provably equal before should still be equal, so why is it ok for the proof of equality to now fail? Doesn't this violate stability under substitution? Cheers, -- P<br>
</blockquote>
<br></span>
It is because of things such as this that I prefer to restrict my usage of Agda to a fragment corresponding to a well-understood type theory.<br>
<br>
This may be limiting in terms of expressivity, conciseness, and efficiency, but at least one can tell whether something is a bug or not, rather than a bug or a feature.<br>
<br>
:-)<span class="HOEnZb"><font color="#888888"><br>
Martin<br>
<br>
</font></span></blockquote></div><br></div>