[Agda] Transitive-on

[Wolfram Kahl]

On Thu, Nov 17, 2011 at 01:29:21PM +0000, Ramana Kumar wrote:
 > I am getting yellow highlighting in the following, which I think
 > indicates a problem.
 > But I don't know what the problem might be or have any idea how to
 > find out by asking Agda directly...

If you installed also Agda-executable (in src/main),
you can use the command ``agda -i . -i <stdlib-location>/src MyModule.lagda''
to type-check your development,
that is, to ``ask Agda directly''.
(Or ``MyModule.agda'', if your are not using literate style (yet ;-)...)

 > What does yellow actually mean

Technically, it means unresolved metavariables.
Usually, it means that Agda could not identify everything we left implicit.

 > , and how can it be resolved?

By making it explicit.
Perhaps we need to replace some ``_'' with an actual argument,
perhaps we need to explicitly supply an implicit argument via ``{arg}'',
sometimes more conveniently ``{x = arg}'' where ``x'' is the name
of the formal parameter in the definition of the caller.

The list of unresolved metavariables in the Goal buffer in Emacs
contains location and type information that MAY help to find out
which implicit argument needs to be explicitly supplied.

(If that list also contained the argument name,
 that would be sooo helpful --- optimistic feature request...)

Locations are also provided by the error message produced by the agda command,
and frequently that is enough --- you just go there and look hard...



Wolfram