[Agda] hidden agda options / getting more info about unsolved metas
Andreas Abel
andreas.abel at ifi.lmu.de
Fri Jan 20 22:32:42 CET 2017
My emacs agda gives me
_0 : .Agda.Primitive.Level [ at
/home/abel/tmp/agda-issue-2327/test/bugs/HighlightU.agda:2,50-51 ]
in the *All Goals* buffer.
On 20.01.2017 22:24, Martin Stone Davis wrote:
> postulate
> yellow-highlighting-but-no-error-message : Set _
>
> Command-line agda reports "unsolved metas" and gives a source-code
> location, but no information about the nature of the unsolved metas.
> Emacs agda gives only yellow-highlighting. I would think that Agda could
> report the type of the unsolved meta (in this case,
> `.Agda.Primitive.Level`). Is there a verbosity option to make that happen?
>
> I've seen some options (iirc, "--tc:100", e.g.) that are not listed by
> "agda --help". Where might I find these "developer" options listed?
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
--
Andreas Abel <>< Du bist der geliebte Mensch.
Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden
andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/
More information about the Agda
mailing list