From 0db6c13af8b25a6e21c9531648ca5ac67c759ad8 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Fri, 15 Jul 2011 19:00:59 -0400 Subject: Preserve tutorial indentation --- doc/intro.ur | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) (limited to 'doc/intro.ur') diff --git a/doc/intro.ur b/doc/intro.ur index b9b15b72..b90e2214 100644 --- a/doc/intro.ur +++ b/doc/intro.ur @@ -74,7 +74,7 @@ fun compose [a] [b] [c] (f : b -> c) (g : a -> b) (x : a) : c = f (g x) compose inc inc 3 (* end *) -(* The "option" type family is like ML's "option" or Haskell's "maybe." Note that, while Ur follows most syntactic conventions of ML, one key difference is that type families appear before their arguments, as in Haskell. *) +(* The "option" type family is like ML's "option" or Haskell's "maybe." We also have a "case" expression form lifted directly from ML. Note that, while Ur follows most syntactic conventions of ML, one key difference is that type families appear before their arguments, as in Haskell. *) fun predecessor (n : int) : option int = if n >= 1 then Some (n - 1) else None @@ -92,3 +92,21 @@ predecessor 6 (* begin eval *) predecessor 0 (* end *) + +(* Naturally, there are lists, too! *) + +val numbers : list int = 1 :: 2 :: 3 :: [] +val strings : list string = "a" :: "bc" :: [] + +fun length [a] (ls : list a) : int = + case ls of + [] => 0 + | _ :: ls' => 1 + length ls' + +(* begin eval *) +length numbers +(* end *) + +(* begin eval *) +length strings +(* end *) -- cgit v1.2.3