<html>
<head>
<meta content="text/html; charset=utf-8" http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
I'd like to ask a related (I hope) question: what is the
paradigmatic simple example where inspect fails, but inspect on
steroids succeeds?<br>
<br>
Thanks,<br>
Aaron<br>
<br>
<div class="moz-cite-prefix">On 12/29/2014 08:25 AM, Andrés
Sicard-Ramírez wrote:<br>
</div>
<blockquote
cite="mid:CAOUWSGBb_=JStcqbLCP3rPXzzpYe4E=g+tD759hK94o7gvX6+A@mail.gmail.com"
type="cite">
<div dir="ltr">
<div class="gmail_extra"><br>
<div class="gmail_quote">On 29 December 2014 at 08:59, Andreas
Abel <span dir="ltr"><<a moz-do-not-send="true"
href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>></span>
wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0
.8ex;border-left:1px #ccc solid;padding-left:1ex">
<div id=":27r" class="a3s" style="overflow:hidden">The way
to proceed here would be<br>
<br>
* check the standard library with your simplified Reveal<br>
* check your own projects and maybe some others you get
hold of<br>
* submit a pull request to agda/agda-stdlib on github.<br>
</div>
</blockquote>
</div>
<br>
<div class="gmail_default" style="font-size:small">In the
last step, please submit your pull request using the 2.4.2.1
branch.<br>
</div>
<br>
-- <br>
<div class="gmail_signature">
<div dir="ltr">Andrés<br>
</div>
</div>
</div>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
</body>
</html>