<div dir="ltr">You want the ability to reduce Agda Terms, then? You could just see if you could manage to expose the internal Agda normalisation procedure as a function from Term to Term? I guess that would be a welcome addition?<div><br></div><div>Pepijn</div></div><div class="gmail_extra"><br><div class="gmail_quote">On 15 June 2015 at 20:36, Philipp Hausmann <span dir="ltr">&lt;<a href="mailto:philipp.hausmann@314.ch" target="_blank">philipp.hausmann@314.ch</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
  
    
  
  <div bgcolor="#FFFFFF" text="#000000">
    <div>Beta redexes are exactly what I want to
      use.... :-(<br>
      <br>
      Back to the drawing board then...<span class="HOEnZb"><font color="#888888"><br>
      <br>
      Philipp</font></span><div><div class="h5"><br>
      <br>
      On 06/15/2015 08:15 PM, Ulf Norell wrote:<br>
    </div></div></div><div><div class="h5">
    <blockquote type="cite">
      <div dir="ltr">Could be there is...
        <div><br>
        </div>
        <div><a href="https://github.com/UlfNorell/agda-prelude/blob/master/src/Tactic/Reflection/Substitute.agda#L60-74" target="_blank">https://github.com/UlfNorell/agda-prelude/blob/master/src/Tactic/Reflection/Substitute.agda#L60-74</a><br>
        </div>
        <div><br>
        </div>
        <div>The syntax doesn&#39;t admit beta redexes, and reducing a beta
          redex isn&#39;t guaranteed to terminate, so</div>
        <div>you need to prove that the function term is &#39;safe&#39; (i.e. is
          not a lambda).</div>
        <div><br>
        </div>
        <div>/ Ulf</div>
      </div>
      <div class="gmail_extra"><br>
        <div class="gmail_quote">On Mon, Jun 15, 2015 at 7:06 PM, Pepijn
          Kokke <span dir="ltr">&lt;<a href="mailto:pepijn.kokke@gmail.com" target="_blank">pepijn.kokke@gmail.com</a>&gt;</span>
          wrote:<br>
          <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
            <div dir="ltr">Hey Philipp,
              <div><br>
              </div>
              <div>You should be able to check whether you&#39;re dealing
                with a defined name or a constructor using
                Reflection.definition. That should set you well on your
                way to defining the &quot;app&quot; function you&#39;re looking for.</div>
              <div><br>
              </div>
              <div>In addition, I would check Ulf&#39;s prelude, if I were
                you. There&#39;s a chance there&#39;s something in there that
                already does this.</div>
              <div><br>
              </div>
              <div>Regards,</div>
              <div>Pepijn</div>
            </div>
            <div>
              <div>
                <div class="gmail_extra"><br>
                  <div class="gmail_quote">On 15 June 2015 at 18:50,
                    Philipp Hausmann <span dir="ltr">&lt;<a href="mailto:philipp.hausmann@314.ch" target="_blank">philipp.hausmann@314.ch</a>&gt;</span>
                    wrote:<br>
                    <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi
                      all,<br>
                      <br>
                      I&#39;m currently trying to use Agda&#39;s Reflection to
                      produce code fragments<br>
                      at compile time, but the limited syntax<br>
                      of Agda&#39;s Reflection makes this rather difficult.
                      Most importantly,<br>
                      there is no generalized application &quot;app Term
                      [Args]&quot;.<br>
                      <br>
                      There is &quot;def Name [Args]&quot; for applying something
                      to named definitions<br>
                      and &quot;var Index [Args]&quot; for applying to de-bruijn
                      indexed variables,<br>
                      but applying to a Term in general (&quot;app Term
                      [Args]&quot;) is not possible<br>
                      right now.<br>
                      <br>
                      There is a clever trick which helps in some cases
                      (&quot;quote ((unquote t1)<br>
                      (unquote t2))&quot;), but that only works if t1 and t2
                      are closed terms.<br>
                      <br>
                      Does anybody know a way to &quot;fake&quot; general
                      application in Agda&#39;s<br>
                      Reflection mechanism?<br>
                      <br>
                      I also have looked into adding an additional
                      general &quot;app Term [Args]&quot;<br>
                      construct to Agda&#39;s Reflection mechanism, which
                      seems to be<br>
                      straightforward. But I&#39;m not really sure if this
                      is a good idea or not...<br>
                      Agda changes:<br>
                      <a href="https://github.com/phile314/agda/commit/80aa35b74eeee794b2f0b8b9dde5d6d32d4c9562" rel="noreferrer" target="_blank">https://github.com/phile314/agda/commit/80aa35b74eeee794b2f0b8b9dde5d6d32d4c9562</a><br>
                      Example using this: <a href="https://gist.github.com/phile314/0a7711a9848b9a81f6f2" rel="noreferrer" target="_blank">https://gist.github.com/phile314/0a7711a9848b9a81f6f2</a><br>
                      <br>
                      Does anybody know any tricks or solution for this?<br>
                      <br>
                      All the best,<br>
                      Philipp<br>
                      <br>
                      _______________________________________________<br>
                      Agda mailing list<br>
                      <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
                      <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
                    </blockquote>
                  </div>
                  <br>
                </div>
              </div>
            </div>
            <br>
            _______________________________________________<br>
            Agda mailing list<br>
            <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
            <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
            <br>
          </blockquote>
        </div>
        <br>
      </div>
    </blockquote>
    <br>
  </div></div></div>

</blockquote></div><br></div>