> Laszlo Nemeth wrote:
> Hi Sebastian,
>
> Thanks for the solution! Though ten minutes ago I almost wrote a reply,
> 'yeah, but it doesn't work!'.
Note that it's not my solution. I just typed Conors funny bracketing
into ascii. But i shouldn't have kicked out your explicit mentioning of
Vecs type parameter.
------------------------------------------------------------------------------
( m, n : Nat ; X : * ; xs : Vec m X ; ys : Vec n X !
let !-----------------------------------------------------!
! vrevacc _m _n _X xs ys : Vec (plus m n) X )
vrevacc _ m _ n _ X xs ys <= rec xs
{ vrevacc _ m _ n _ X xs ys <= case xs
{ vrevacc _ zero _ n _ X vnil ys => ys
vrevacc _ (suc m) _ n _ X (vcons x xs) ys
=>
typecast (respEq (lam n => Vec n X) (plusSuc m n))
% (vrevacc xs (vcons x ys))
}
}
------------------------------------------------------------------------------
I've attached a version that elaborates successfully on my machine. If
this is a positioning of implicit arguments issue is beyond my scope.
Best regards,
Sebastian
------------------------------------------------------------------------------
( n : Nat !
data (---------! where (------------! ; !-------------!
! Nat : * ) ! zero : Nat ) ! suc n : Nat )
------------------------------------------------------------------------------
( n : Nat ; X : * ! ( x : X ; xs : Vec n X !
data !------------------! where (--------------! ; !-----------------------!
! Vec n X : * ) ! vnil : ! ! vcons x xs : !
! Vec zero X ) ! Vec (suc n) X )
------------------------------------------------------------------------------
( m, n : Nat !
let !----------------!
! plus m n : Nat )
plus m n <= rec m
{ plus m n <= case m
{ plus zero n => n
plus (suc m) n => suc (plus m n)
}
}
------------------------------------------------------------------------------
( f : A -> B ; p : a = b !
let !-------------------------!
! respEq f p : f a = f b )
respEq f p <= case p
{ respEq f refl => refl
}
------------------------------------------------------------------------------
( m, n : Nat !
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 => respEq suc (plusSuc m n)
}
}
------------------------------------------------------------------------------
( Q : S = T ; s : S !
let !--------------------!
! typecast Q s : T )
typecast Q s <= case Q
{ typecast refl s => s
}
------------------------------------------------------------------------------
( m, n : Nat ; X : * ; xs : Vec m X ; ys : Vec n X !
let !-----------------------------------------------------!
! vrevacc _m _n _X xs ys : Vec (plus m n) X )
vrevacc _ m _ n _ X xs ys <= rec xs
{ vrevacc _ m _ n _ X xs ys <= case xs
{ vrevacc _ zero _ n _ X vnil ys => ys
vrevacc _ (suc m) _ n _ X (vcons x xs) ys
=>
typecast (respEq (lam n => Vec n X) (plusSuc m n))
% (vrevacc xs (vcons x ys))
}
}
------------------------------------------------------------------------------
