Thanks, have renamed both to Cons_nth_drop_Suc.
Tobias
On 09/09/2014 15:33, Christian Sternagel wrote:
> Dear all,
>
> just an observation. The facts
>
> List.drop_Suc_conv_tl:
> ?i < length ?xs ⟹
> ?xs ! ?i # drop (Suc ?i) ?xs = drop ?i ?xs
> List.nth_drop':
> ?i < length ?xs ⟹
Dear all,
just an observation. The facts
List.drop_Suc_conv_tl:
?i < length ?xs ⟹
?xs ! ?i # drop (Suc ?i) ?xs = drop ?i ?xs
List.nth_drop':
?i < length ?xs ⟹
?xs ! ?i # drop (Suc ?i) ?xs = drop ?i ?xs
are duplicates of each other.
cheers
chris
