--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Example.hs Tue Mar 03 17:05:18 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-{-# OPTIONS_GHC -fglasgow-exts #-}
-
-module Example where {
-
-
-foldla :: forall a b. (a -> b -> a) -> a -> [b] -> a;
-foldla f a [] = a;
-foldla f a (x : xs) = foldla f (f a x) xs;
-
-rev :: forall a. [a] -> [a];
-rev xs = foldla (\ xsa x -> x : xsa) [] xs;
-
-list_case :: forall t a. t -> (a -> [a] -> t) -> [a] -> t;
-list_case f1 f2 (a : list) = f2 a list;
-list_case f1 f2 [] = f1;
-
-data Queue a = AQueue [a] [a];
-
-empty :: forall a. Queue a;
-empty = AQueue [] [];
-
-dequeue :: forall a. Queue a -> (Maybe a, Queue a);
-dequeue (AQueue [] []) = (Nothing, AQueue [] []);
-dequeue (AQueue xs (y : ys)) = (Just y, AQueue xs ys);
-dequeue (AQueue (v : va) []) =
- let {
- (y : ys) = rev (v : va);
- } in (Just y, AQueue [] ys);
-
-enqueue :: forall a. a -> Queue a -> Queue a;
-enqueue x (AQueue xs ys) = AQueue (x : xs) ys;
-
-}