Naming return value in Idris?

Question

In Idris, one can explicitly name arguments in function type declarations, like

length : (str : String) -> Nat

But when I try to name the return value, like in

length : (str : String) -> (lengthOfStr : Nat)

the idris compiler throws an error

unexpected end of input expecting "->"

Why doesn't the same syntax for naming arguments work for return values? Is there a way to name return values in Idris (so they can be referenced in the doc-string)?

Answer 1

No, that's not possible, see this issue. Your question about doc-string might change some opinions, why not ask there? But there might be a problem: someone might think that e.g. f: (n : Nat) -> (n : Nat) is valid and would only allow f n = n as an implementation. But you can't specify the return value, only the return type.