Hi Serguey
And here I got stuck:
----------------------------------------------------------------------
--------
( X : * ; xs : Vec (succ n) X !
let !------------------------------!
! vecInit xs : Vec n X )
vecInit xs <= case xs
{ vecInit (vcons n' ns) => vcons n' (vecInit ns)
}
----------------------------------------------------------------------
--------
This is a version of init function from Haskell Prelude:
init [x] = []
init (x:xs) = x:init xs
I do not get second case from Epigram when elaborating. And, actually,
Epigram does not like "=> vcons n' (vecInit ns)" part. But I can
understand that, albeit not formally.
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.
Where should I look for hints on to get a clue on how to do it right?
The tail of the list!
All the best
Conor
This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.
