[Agda] How to write a type alias for _->_?

[David Banas]

Hi all,

I’m trying to define a type alias for function arrow: _->_, and can’t make it work.
Here’s my code:

_⇒_ : ∀ {A B : Set} → A → B → Set₁
_⇒_ A B = {!A → B!}

And, when I type `C-c C-<SPACE>` in the hole, the “A” gets highlighted in red and I’m told:

A₁ should be a sort, but it isn't
when checking that the expression A has type _3

which I don’t really understand.

Can anyone shed some light?

Thanks,
-db

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210120/3117404b/attachment.html>