How do I split a type declaration into multiple lines in Idris? Types should drive development. So they may become quite long and not fit on screen. Like this one:
addMatrices : (augent : Vect rowCount (Vect columnCount element)) -> (addend: Vect rowCount (Vect columnCount element)) -> Vect rowCount (Vect columnCount element)
To do it with formatting only, you can do it as you've done,
addMatrices : (augent : Vect rowCount (Vect columnCount element)) ->
(addend: Vect rowCount (Vect columnCount element)) ->
Vect rowCount (Vect columnCount element)
The docs say
New declarations must begin at the same level of indentation as the preceding declaration.
Similarly, the book only says, in Section 2.4.1 Whitespace significance: the layout rule,
... in any list of definitions and declarations, all must begin in precisely the same column.
Since the new line isn't a new declaration, I take this to mean the new line can start at any level of indentation, so
addMatrices : (augent : Vect rowCount (Vect columnCount element)) ->
(addend: Vect rowCount (Vect columnCount element)) ->
Vect rowCount (Vect columnCount element)
and other variants would also be valid.
Alternatively, following on from Al.G.'s comment, you can use a type alias, but if rowCount and columnCount aren't in scope, which I'm guessing they aren't for you, you'll need a type-level function, which is a generalisation of a type alias. It's a function that returns a type.
Matrix : Nat -> Nat -> Type -> Type
Matrix rows cols elem = Vect rows (Vect cols elem)
Then you'll have
addMatrices : (augent : Matrix rowCount columnCount element) ->
(addend: Matrix rowCount columnCount element) ->
Matrix rowCount columnCount element
which isn't much shorter.
To be honest, I'd look at using shorter names and take advantage of any obvious context
addMatrices : (augent : Vect r (Vect c elem)) -> (addend: Vect r (Vect c elem)) -> Vect r (Vect c elem)