18 Sep
2006
18 Sep
'06
6:53 p.m.
On Mon, Sep 18, 2006 at 12:23:11AM +0100, Ross Paterson wrote:
To prove that (even for partial and infinite lists ps)
splitSeq ps = [(a, seconds a ps) | a <- nub ps]
[...] we can establish, by induction on the input list,
(1) fst (splitSeq' s ps) = [(a, seconds a ps) | a <- nub ps, not (member a s)] (2) member x s => get x s (snd (splitSeq' s ps)) = seconds x ps
Oops, nub ps should be nub (map fst ps) in each case.