[Agda] Instance resolution question

[Ulf Norell]

The candidates are not equal. This is what `rob` expands to:

rob : CPF
rob {{ctx}} = fun (λ {{ctx'}} → e)

ctx and ctx' are distinct variables.

/ Ulf

On Wed, Mar 28, 2018 at 6:39 AM, Apostolis Xekoukoulotakis <
apostolis.xekoukoulotakis at gmail.com> wrote:

> ```
> module Test2 where
>
>
> data A : Set where
>
>
> CPF : Set
> CPF = {{a : A}} → A
>
> postulate
>   fun : CPF → CPF
>   e : CPF
>
>
> bob : CPF
> bob {{ctx}} = fun (e {{ctx}})
>
>
> rob : CPF
> rob = fun e
>
> ```
>
> I wonder if there is a way to write "rob" instead of "bob".
>
> Keep in mind that the candidates are definitionally equal. (it seems)
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180328/b665f883/attachment.html>