<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">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@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>```<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>______________________________<wbr>_________________<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/<wbr>mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>