<div dir="ltr"><div><div><a href="https://lists.chalmers.se/pipermail/agda/2017/009802.html">https://lists.chalmers.se/pipermail/agda/2017/009802.html</a><br><br></div>From a previous discussion with Andreas, hidden/instance arguments are inserted eagerly.<br></div><div>I wonder  if I can disable this specifically for "{{ctx}}".<br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Mar 28, 2018 at 8:14 AM, Ulf Norell <span dir="ltr"><<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@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"><div><div>The candidates are not equal. This is what `rob` expands to:<br><br>rob : CPF<br>rob {{ctx}} = fun (λ {{ctx'}} → e)<br><br></div>ctx and ctx' are distinct variables.<br><br></div>/ Ulf<br></div><div class="gmail_extra"><br><div class="gmail_quote"><div><div class="h5">On Wed, Mar 28, 2018 at 6:39 AM, Apostolis Xekoukoulotakis <span dir="ltr"><<a href="mailto:apostolis.xekoukoulotakis@gmail.com" target="_blank">apostolis.xekoukoulotakis@<wbr>gmail.com</a>></span> wrote:<br></div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5"><div dir="ltr"><div><div>```<br>module Test2 where<br><br><br>data A : Set where<br><br><br>CPF : Set<br>CPF = {{a : A}} → A<br><br>postulate<br>  fun : CPF → CPF<br>  e : CPF<br>  <br><br>bob : CPF<br>bob {{ctx}} = fun (e {{ctx}})<br><br><br>rob : CPF<br>rob = fun e <br><br>```<br><br></div>I wonder if there is a way to write "rob" instead of "bob".<br><br></div>Keep in mind that the candidates are definitionally equal. (it seems)<br></div>
<br></div></div>______________________________<wbr>_________________<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/mail<wbr>man/listinfo/agda</a><br>
<br></blockquote></div><br></div>
</blockquote></div><br></div>