[Agda] a question about name parts

[Andrés Sicard-Ramírez]

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?


-- 
Andrés
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080319/ee0ed23b/attachment.html