[Agda] what is status of → ?

[Nils Anders Danielsson]

On 2011-02-11 11:15, Permjacov Evgeniy wrote:
> When I give Agda _→_ as value (for example, as parameter for type
> family) I get an error. So, is → a special synthax form and is there any
> 'standart' type constructor to be used as replacement ?

You can define a type constructor as follows:

   Π : (A : Set) → (A → Set) → Set
   Π A B = (x : A) → B x

(Or use lambdas.)

-- 
/NAD