doc-src/Codegen/Thy/examples/example.ML
changeset 34156 3a7937841585
parent 33707 68841fb382e0
child 37610 1b09880d9734
equal deleted inserted replaced
34155:14aaccb399b3 34156:3a7937841585
     1 structure Example = 
     1 structure Example : sig
     2 struct
     2   val foldl : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a
       
     3   val rev : 'a list -> 'a list
       
     4   val list_case : 'a -> ('b -> 'b list -> 'a) -> 'b list -> 'a
       
     5   datatype 'a queue = AQueue of 'a list * 'a list
       
     6   val empty : 'a queue
       
     7   val dequeue : 'a queue -> 'a option * 'a queue
       
     8   val enqueue : 'a -> 'a queue -> 'a queue
       
     9 end = struct
     3 
    10 
     4 fun foldl f a [] = a
    11 fun foldl f a [] = a
     5   | foldl f a (x :: xs) = foldl f (f a x) xs;
    12   | foldl f a (x :: xs) = foldl f (f a x) xs;
     6 
    13 
     7 fun rev xs = foldl (fn xsa => fn x => x :: xsa) [] xs;
    14 fun rev xs = foldl (fn xsa => fn x => x :: xsa) [] xs;