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

[Nils Anders Danielsson]

On 2009-08-14 22:56, Noam Zeilberger wrote:
> On Fri, Aug 14, 2009 at 5:17 PM, Noam
> Zeilberger<noam.zeilberger at gmail.com> wrote:
>>  Is there an easy way to check whether a name denotes a
>> type constructor?
> 
> and the answer to this seems to be, "Have a look at isDatatype in
> Agda.TypeChecking.Positivity".

My guess is that you want to use something slightly more liberal than
that function (unless "dataClause" is relevant for your purposes), but
using getConstInfo seems like a good idea.

-- 
/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.