[Agda] Why are some terms in the Agda goal report colored blue?

James Wood james.wood.100 at strath.ac.uk
Wed Jan 13 21:30:22 CET 2021


Hi David,

If I remember correctly, the blue vs black difference is something 
really silly, like that names with non-ASCII characters have a different 
colour to all-ASCII names. You might want to see whether that's it.

All the best,
James

On 31/12/2020 22:40, David Banas wrote:
> CAUTION: This email originated outside the University. Check before 
> clicking links or attachments.
> Hi all,
> 
> What's the significance of some of the terms in the Agda goal report (in 
> response to: `C-c C-,` in Emacs) being colored blue?
> 
> Thanks,
> -db
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 



More information about the Agda mailing list