diff doc/intro.ur @ 1525:a479947efbcd

Improve detection of XML in urweb-mode; small tutorial improvement
author Adam Chlipala <adam@chlipala.net>
date Tue, 02 Aug 2011 17:28:37 -0400
parents 5616b2cbdcdb
children 2d9f831d45c9
line wrap: on
line diff
--- a/doc/intro.ur	Tue Aug 02 17:04:14 2011 -0400
+++ b/doc/intro.ur	Tue Aug 02 17:28:37 2011 -0400
@@ -259,20 +259,24 @@
     con t :: Type -> Type
     val empty : a ::: Type -> t a
     val push : a ::: Type -> t a -> a -> t a
-    val pop : a ::: Type -> t a -> option a
+    val peek : a ::: Type -> t a -> option a
+    val pop : a ::: Type -> t a -> option (t a)
 end
 
 structure Stack : STACK = struct
     con t = list
     val empty [a] = []
     fun push [a] (t : t a) (x : a) = x :: t
+    fun peek [a] (t : t a) = case t of
+                                 [] => None
+                               | x :: _ => Some x
     fun pop [a] (t : t a) = case t of
-                                [] => None
-                              | x :: _ => Some x
+                                 [] => None
+                               | _ :: t' => Some t'
 end
 
 (* begin eval *)
-Stack.pop (Stack.push (Stack.push Stack.empty "A") "B")
+Stack.peek (Stack.push (Stack.push Stack.empty "A") "B")
 (* end *)
 
 (* Ur also inherits the ML concept of <b>functors</b>, which are functions from modules to modules. *)