[Agda] Agda2 emacs mode - yellow highlighting

[Nils Anders Danielsson]

On 2019-12-03 12:38, Andrew Pitts wrote:
> If I select a piece of yellow-highlighted code, is there a command to
> replace the region with code in which all implicit arguments are made
> made visible as holes?

No. I guess this would be impossible to implement, because there could
be ambiguous constructors or fields in the region.

> Supplementary question: there is a global command in Agda2
> 
> C-c C-x C-h (Toggle display of hidden arguments)
> 
> Can someone give me an example of what it is supposed to do? (I
> naively thought it might display all the hidden arguments.)

After you have turned on this option the output of various commands
includes hidden arguments. Note that the setting resets to the default
when the file is loaded.

-- 
/NAD