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. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
