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

[Noam Zeilberger]

[seems I forgot to CC this to the list...]

---------- Forwarded message ----------
From: Noam Zeilberger <noam.zeilberger at gmail.com>
Date: Fri, Aug 14, 2009 at 2:08 PM
Subject: Re: [Agda] constructor/definition taxonomy in compiler
internals/syntax highlighting
To: Nils Anders Danielsson <nad at cs.nott.ac.uk>


On Fri, Aug 14, 2009 at 8:28 AM, Nils Anders
Danielsson<nad at cs.nott.ac.uk> wrote:
> 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.

well, yes, that is a difference between term constructors and type
constructors.  I guess my question is really, why doesn't the internal
taxonomy maintain a distinction between type constructors (i.e.,
things like Nat, List, etc.) and [type definitions, but maybe
"definition" is ambiguous here, so let's call them] type-valued
functions (i.e., things like Reflexive in Logic.Relations)?  Or at
least it doesn't at the level where I was looking (in
Agda.Syntax.Scope.Monad and in the syntax highlighting).  It must at
some level.  Is there an easy way to check whether a name denotes a
type constructor?

>> I ask because I'm trying to write a new compiler module,
>
> Sounds interesting. Would you like to describe what you intend to do?

Automated translation from Agda source to another friendly proof
assistant.  (But I'm still trying to figure out whether it can
actually be done...)

Noam