[Agda] hidden agda options / getting more info about unsolved metas

[Martin Stone Davis]

duh... "-v 100" is listed by 'agda --help'.


On 01/20/2017 01:24 PM, 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?
>