<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">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't admit beta redexes, and reducing a beta redex isn't guaranteed to terminate, so</div><div>you need to prove that the function term is 'safe' (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"><<a href="mailto:pepijn.kokke@gmail.com" target="_blank">pepijn.kokke@gmail.com</a>></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're dealing with a defined name or a constructor using Reflection.definition. That should set you well on your way to defining the "app" function you're looking for.</div><div><br></div><div>In addition, I would check Ulf's prelude, if I were you. There's a chance there's something in there that already does this.</div><div><br></div><div>Regards,</div><div>Pepijn</div></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On 15 June 2015 at 18:50, Philipp Hausmann <span dir="ltr"><<a href="mailto:philipp.hausmann@314.ch" target="_blank">philipp.hausmann@314.ch</a>></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'm currently trying to use Agda's Reflection to produce code fragments<br>
at compile time, but the limited syntax<br>
of Agda's Reflection makes this rather difficult. Most importantly,<br>
there is no generalized application "app Term [Args]".<br>
<br>
There is "def Name [Args]" for applying something to named definitions<br>
and "var Index [Args]" for applying to de-bruijn indexed variables,<br>
but applying to a Term in general ("app Term [Args]") is not possible<br>
right now.<br>
<br>
There is a clever trick which helps in some cases ("quote ((unquote t1)<br>
(unquote t2))"), but that only works if t1 and t2 are closed terms.<br>
<br>
Does anybody know a way to "fake" general application in Agda's<br>
Reflection mechanism?<br>
<br>
I also have looked into adding an additional general "app Term [Args]"<br>
construct to Agda's Reflection mechanism, which seems to be<br>
straightforward. But I'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">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>