# HG changeset patch # User haftmann # Date 1261553474 -3600 # Node ID 0928909af6aa666614ad9ab958784ceb13306102 # Parent 254ac75e4c383adba96967e1eb9091b053672b19 updated generated examples diff -r 254ac75e4c38 -r 0928909af6aa doc-src/Codegen/Thy/examples/Example.hs --- a/doc-src/Codegen/Thy/examples/Example.hs Wed Dec 23 08:31:14 2009 +0100 +++ b/doc-src/Codegen/Thy/examples/Example.hs Wed Dec 23 08:31:14 2009 +0100 @@ -2,7 +2,6 @@ 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; diff -r 254ac75e4c38 -r 0928909af6aa doc-src/Codegen/Thy/examples/example.ML --- a/doc-src/Codegen/Thy/examples/example.ML Wed Dec 23 08:31:14 2009 +0100 +++ b/doc-src/Codegen/Thy/examples/example.ML Wed Dec 23 08:31:14 2009 +0100 @@ -1,5 +1,12 @@ -structure Example = -struct +structure Example : sig + val foldl : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a + val rev : 'a list -> 'a list + val list_case : 'a -> ('b -> 'b list -> 'a) -> 'b list -> 'a + datatype 'a queue = AQueue of 'a list * 'a list + val empty : 'a queue + val dequeue : 'a queue -> 'a option * 'a queue + val enqueue : 'a -> 'a queue -> 'a queue +end = struct fun foldl f a [] = a | foldl f a (x :: xs) = foldl f (f a x) xs;