<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">&lt;<a moz-do-not-send="true"
                href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>&gt;</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>