[Agda] How to read constraints?

[Ulf Norell]

On Wed, Aug 19, 2009 at 10:39 AM, Robin Green <greenrd at greenrd.org> wrote:

> I do not understand the output of the Show Constraints command, and I
> cannot find a reference for it.
>

Yes, the printing of the constraints could use some tidying.

Here is what it prints:
>
> _403 := λ F' G' H' GF' {d'} {a'} {b'} {c'} h' g' f' GFD' →
>  composition h' (λ x → g' (f' x))  |  [record {domain = a; codomain =
>  d; fn = λ x → h (g (f x))} = ?0 F G H GF h g f GFD : Function]
>
> What does this mean?
>

These kinds of constraints have the form

Meta := λ FreeVars → TermThatYouWrote | [ LHS = RHS : Type ]

and basically says that in order for TermThatYouWrote to be accepted the
constraint LHS = RHS has to be resolved. In this case it seems there is an
open hole (?0) that needs to be filled in.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090821/6d96c7d4/attachment.html