Hi hol-info,
I want to ask whether anyone thinks these are good automatic rewrites in
listTheory?
|- (∀n. TAKE n [] = []) ∧
∀n x xs. TAKE n (x::xs) = if n = 0 then [] else x::TAKE (n − 1) xs
|- (∀n. DROP n [] = []) ∧
∀n x xs. DROP n (x::xs) = if n = 0 then x::xs else DROP (n − 1) xs
I find them annoying because they introduce a conditional, which then
causes subgoal splits when rewriting (with rw or srw_tac). While they are
sometimes good rewrites, I don't think they should be _automatic_, as they
currently are.
Shall we remove them from srw_ss?
On another note, is there a way to remove things from srw_ss after they
have been added? I see only how to do that for named fragments (which I
don't think the above rewrites are in one of).
Ramana
------------------------------------------------------------------------------
Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San
Francisco, CA to explore cutting-edge tech and listen to tech luminaries
present their vision of the future. This family event has something for
everyone, including kids. Get more information and register today.
http://sdm.link/attshape
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
