[Agda] a question about name parts

[Ulf Norell]

On Wed, Mar 19, 2008 at 4:06 PM, Andrés Sicard-Ramírez <
andres.sicard at gmail.com> wrote:

> Hi,
>
> I tried to define a function
>
> ' : Nat -> Nat
> ' = ...
>
> but I got an Agda error:  character literal must contain a single
> character
>
> In Ulf's thesis I could not find any restriction to use ' as name part.
> So, is it a bug or ' should be added to the reserved words?


It's even more restricted: a name part cannot start with '. Backquote is
fine though.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080319/dde80b0d/attachment.html