Re: [Agda] what is status of → ?

Jean-Philippe Bernardy bernardy at chalmers.se
Fri Feb 11 11:38:48 CET 2011


On Fri, Feb 11, 2011 at 11:15 AM, Permjacov Evgeniy <permeakra at gmail.com> wrote:
> When I give Agda _→_ as value (for example, as parameter for type
> family) I get an error. So, is → a special synthax form

Yes, it's an alias for ->

and is there any
> 'standart' type constructor to be used as replacement ?

Not as far as I know.

Cheers,
-- JP


More information about the Agda mailing list