[Agda] constructor/definition taxonomy in compiler internals/syntax highlighting

[Nils Anders Danielsson]

On 2009-08-14 01:11, Noam Zeilberger wrote:
> My question is, how come type *constructors* are treated as
> definitions?

Presumably because you cannot use them for pattern matching.

> I ask because I'm trying to write a new compiler module,

Sounds interesting. Would you like to describe what you intend to do?

> where I think treating type constructor names as ConstructorName's
> would make more sense.

If you need to view terms in a different way, then I suggest that you
define a suitable view. (As an example, see
Agda.TypeChecking.EtaContract.BinAppView/binAppView.)

-- 
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.