Hi,
I'm trying to complete the definition of sized reverse with accumulator,
and can't figure out where the proof of (1+m)+m'=m+(1+m') goes. The
syntax given in 'Epigram: practical programming...' doesn't seem to
work. I tried to make all implicit arguments visible in the hope that I
can plug in the new length somewhere, but the rhs remains brown!
I guess I don't fully understand implicit parameters yet.
Any help, or pointers are much appreciated.
Thanks. Laszlo
PS. This is with the version from sneezy.
------------------------------------------------------------------------------
( _m : Nat ; _X : * ; xs : Vec m X ; _n : Nat ; ys : Vec n X !
let !----------------------------------------------------------------!
! vracc _m _X xs _n ys : (Vec (plus m n) X) )
vracc _ n xs _ m ys <= rec xs
{ vracc _ n xs _ m ys <= case xs
{ vracc _ zero _ X vnil _ m ys => ys
vracc _ (suc m) _ X (vcons x xs) _ m' ys
[=> vracc xs (vcons x ys)]
}
}
------------------------------------------------------------------------------
let (---------------------------------------------------!
! plusSuc m n : (plus m (suc n)) = (suc (plus m n)) )
plusSuc m n <= rec m
{ plusSuc m n <= case m
{ plusSuc zero n => refl
plusSuc (suc m) n => respSuc (plusSuc m n)
}
}
