在 idris 中键入函数别名

Question

是否可以在 Idris 中定义类型函数的短别名？

虽然以下代码类型检查，但我希望AugentRow的定义更短。

import Data.Vect
ColumnCount : Type
ColumnCount = Nat
Cell : Type
Cell = Type
Row : ColumnCount -> Cell -> Type
Row   columnCount    cell =  Vect columnCount cell
AugentRow : ColumnCount -> Cell -> Type
AugentRow   columnCount    cell =  Row columnCount cell

一些没有重复的定义，比如这个：

AugentRow = Row

Answer 1

到目前为止我找到的最短形式：

AugentRow : ColumnCount -> Cell -> Type
AugentRow = Row