> It's not known that the length of ns is a succ, so it isn't
> appropriate to
> call vecInit here. The Haskell function is exploiting fall-through
> in patterns
> here, so you should expect the Epigram version to be slightly
> noisier. So far,
> you haven't quite determined which case you're in. You will need to
> look a
> bit harder. You'll also need to indicate what you're doing recursion on.
Yes. I almost used to arriving to the answer the seconds after asking
a question.
( X : * ; xs : Vec (succ n) X !
let !------------------------------!
! vecInit xs : Vec n X )
vecInit xs <= case xs
{ vecInit (vcons n' ns) <= case ns
{ vecInit (vcons n' vnil) => vnil
vecInit (vcons n'' (vcons n' ns)) => vcons n'' (vecInit (vcons n' ns))
}
}
(indentation can be broken, I indented badly pasted version)
I'm looking for more dependent function. Now - with variable length
vector size checking!
(I almost figured out how to do it)
