summaryrefslogtreecommitdiff
path: root/doc/intro.ur
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2011-07-15 18:55:58 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2011-07-15 18:55:58 -0400
commit4b54ea891652138a8d58399bbbfdbb852b70eabd (patch)
tree12f8f5eac9e735909223542818bb3f9fefc70ef0 /doc/intro.ur
parent4593948fd27e6cdc4c24a0b008ce1beac4df2560 (diff)
Make 'static' protocol handle unlimited retry
Diffstat (limited to 'doc/intro.ur')
-rw-r--r--doc/intro.ur19
1 files changed, 19 insertions, 0 deletions
diff --git a/doc/intro.ur b/doc/intro.ur
index d474a1e1..b9b15b72 100644
--- a/doc/intro.ur
+++ b/doc/intro.ur
@@ -73,3 +73,22 @@ fun compose [a] [b] [c] (f : b -> c) (g : a -> b) (x : a) : c = f (g x)
(* begin eval *)
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. *)
+
+fun predecessor (n : int) : option int = if n >= 1 then Some (n - 1) else None
+
+(* begin hide *)
+fun show_option [t] (_ : show t) : show (option t) =
+ mkShow (fn x => case x of
+ None => "None"
+ | Some x => "Some(" ^ show x ^ ")")
+(* end *)
+
+(* begin eval *)
+predecessor 6
+(* end *)
+
+(* begin eval *)
+predecessor 0
+(* end *)