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

Martin Stone Davis martin.stone.davis at gmail.com
Fri Jan 20 22:24:10 CET 2017


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?



More information about the Agda mailing list