
<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">Hi all,<div class=""><br class=""></div><div class="">I’m trying to define a type alias for function arrow: <font face="Menlo" class="">_->_</font>, and can’t make it work.<div class="">Here’s my code:</div><div class=""><br class=""></div><blockquote style="margin: 0 0 0 40px; border: none; padding: 0px;" class=""><div class=""><div class=""><font face="Menlo" class="">_⇒_ : ∀ {A B : Set} → A → B → Set₁</font></div></div><div class=""><div class=""><font face="Menlo" class="">_⇒_ A B = {!A → B!}</font></div></div></blockquote><div class=""><br class=""></div><div class="">And, when I type `<font face="Menlo" class="">C-c C-<SPACE></font>` in the hole, the “A” gets highlighted in red and I’m told:</div><div class=""><br class=""></div><blockquote style="margin: 0 0 0 40px; border: none; padding: 0px;" class=""><div class=""><div class=""><font face="Menlo" class="">A₁ should be a sort, but it isn't</font></div></div><div class=""><div class=""><font face="Menlo" class="">when checking that the expression A has type _3</font></div></div></blockquote><div class=""><br class=""></div><div class="">which I don’t really understand.</div><div class=""><br class=""></div><div class="">Can anyone shed some light?</div><div class=""><br class=""></div><div class="">Thanks,</div><div class="">-db</div><div class=""><br class=""></div></div></body></html>