From 3f9bd117b37c9feb9f37a6e9ac84bbb4697f86d3 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 2 Aug 2011 17:28:37 -0400 Subject: Improve detection of XML in urweb-mode; small tutorial improvement --- doc/intro.ur | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) (limited to 'doc/intro.ur') diff --git a/doc/intro.ur b/doc/intro.ur index 02adfdd2..e3611567 100644 --- a/doc/intro.ur +++ b/doc/intro.ur @@ -259,20 +259,24 @@ signature STACK = sig 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 functors, which are functions from modules to modules. *) -- cgit v1.2.3