CODEWITHSUNDEEP
idris
Alexander Novikov
Alexander Novikov

Reputation: 23

Type Function Aliases in Idris

Is it possible to define a short alias of a type function in Idris?

While the following code type-checks, I'd like to have a shorter definition for 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

Some definition without unnessesory repetition like this one:

AugentRow = Row

Upvotes: 0

Views: 349

Answers (1)

Alexander Novikov
Alexander Novikov

Reputation: 23

The shortest form I've found so far:

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

Upvotes: 1

Related Questions