Sorry for the code presentation, too.
Perhaps it's better to attach a small piece of code :
The last clause was rejected, (I presume) because of the
non-unification of
(suc n) with (plus n (suc zero)). Is that right ?
Is there a way to use some commutatitivy of plus (like using JMeq in
Coq) ? Or any other way to define vrev ?
Cheers,
Pierre
( xs : Vec n X !
let !----------------------!
! vrev _n xs : Vec n X )
vrev _ n xs <= rec xs
{ vrev _ n xs <= case xs
{ vrev _ zero vnil => vnil
vrev _ (suc n) (vcons x xs)
=> vappend _ n (vrev _ n xs) (vcons x vnil)
}
}
