<div dir="ltr"><div>This might work.<br><br></div><div>(I do want cob and not bob).<br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Mar 28, 2018 at 9:30 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>You can wrap CPF in data type/record:<br><br>record CPF : Set where<br>  constructor mkCPF<br>  field unCPF : {{a : A}} → A<span class=""><br><br>postulate<br>  fun : CPF → CPF<br>  e   : CPF<br><br></span><span class="">rob : CPF<br>rob = fun e<br><br></span></div><div>But note that if it's really `bob` you want, not inserting the {{ctx}} will give you `cob`, which<br></div><div>is not the same as `bob`:<br></div><div><br></div><div>cob : CPF<br>cob {{ctx}} = fun (λ {{ctx'}} → e {{ctx'}}) {{ctx}}<span class="HOEnZb"><font color="#888888"><br></font></span></div><span class="HOEnZb"><font color="#888888"><div><br></div>/ Ulf<br></font></span></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Mar 28, 2018 at 7:36 AM, Apostolis Xekoukoulotakis <span dir="ltr"><<a href="mailto:apostolis.xekoukoulotakis@gmail.com" target="_blank">apostolis.xekoukoulotakis@<wbr>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><a href="https://lists.chalmers.se/pipermail/agda/2017/009802.html" target="_blank">https://lists.chalmers.se/pipe<wbr>rmail/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="m_-5729635221820527443HOEnZb"><div class="m_-5729635221820527443h5"><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="m_-5729635221820527443m_7189215109865396353h5">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@gma<wbr>il.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="m_-5729635221820527443m_7189215109865396353h5"><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>
</div></div></blockquote></div><br></div>
</div></div></blockquote></div><br></div>