Hi Florian,Would it be possible to set up List.thy so that it uses more of the Haskell prelude list functions? Here's the mapping I'm thinking of (some of these mappings may already be set up, but I know that at least (op @) and rev aren't):
op @ --> (Prelude.++) filter --> Prelude.filter concat --> Prelude.concat foldl --> Prelude.foldlfoldr --> Prelude.foldr (* ...with last two arguments swapped. What to do when foldr is curried? *)
hd --> Prelude.head tl --> Prelude.tail last --> Prelude.last butlast --> Prelude.init map --> Prelude.map take --> Prelude.take drop --> Prelude.drop takeWhile --> Prelude.takeWhile dropWhile --> Prelude.dropWhile rev --> Prelude.reverse zip --> Prelude.zip upt --> (\m n -> [m..(n-1)]) replicate --> Prelude.replicateAnother alternative would be to have a special "Haskell_Prelude" theory that contains these adaptations.
Description: S/MIME cryptographic signature