But unpacking one from a function doesn't seem to have been added to the syntax:
def LowerTriMat (n:Type) [Ix n] (v:Type) : Type = (i:n)=>(..i)=>v
def UpperTriMat (n:Type) [Ix n] (v:Type) : Type = (i:n)=>(i..)=>v
def transpose_lower_to_upper {n v} (lower:LowerTriMat n v) : UpperTriMat n v =
for i j.
(j' ,> i') = transpose_upper_ix i j
lower.j'.i'
Constructing and returning a dependent pair works fine:
But unpacking one from a function doesn't seem to have been added to the syntax:
gives
Inlining the function works.