pref_eq k xs ys = take k xs == take k ys
This seems to be a straightforward implementation with good properties.
Actually, no, at least not if implemented naively.
I choosed this example, since I stumbled on this question last week. Reputable mathematicians doing "combinatorics on words" are using exactly this definition! (Karhumäki, Harju) There are others (Holub), that use the (to the computer scientist) nicer(?) pref_eq 0 _ _ = True pref_eq _ _ [] = False pref_eq _ [] _ = False pref_eq k (x:xs) (y:ys) = x == y && pref_eq (k-1) xs ys And as you guess it, there are lemmata (and probably theorems), that hold for one of the definitions only... Later, the mathematicians agree upton to call the first version "pref_eq" and the second "pref_eq_proper". And yes, you are right, just to change the behavior of take would not solve this issue. My topic was really more like
"don't leap into coding a function before you know what it means"
as you pointed out with nice words :-) This is not the main topic of the thread (is this true?) but we are in a cafe, so from time to time one adds some cents... /BR