comparison doc/intro.ur @ 1498:8c32c7191bf0

Make 'static' protocol handle unlimited retry
author Adam Chlipala <adam@chlipala.net>
date Fri, 15 Jul 2011 18:55:58 -0400
parents 0b639858200b
children 92c929793d0f
comparison
equal deleted inserted replaced
1497:0b639858200b 1498:8c32c7191bf0
71 fun compose [a] [b] [c] (f : b -> c) (g : a -> b) (x : a) : c = f (g x) 71 fun compose [a] [b] [c] (f : b -> c) (g : a -> b) (x : a) : c = f (g x)
72 72
73 (* begin eval *) 73 (* begin eval *)
74 compose inc inc 3 74 compose inc inc 3
75 (* end *) 75 (* end *)
76
77 (* 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. *)
78
79 fun predecessor (n : int) : option int = if n >= 1 then Some (n - 1) else None
80
81 (* begin hide *)
82 fun show_option [t] (_ : show t) : show (option t) =
83 mkShow (fn x => case x of
84 None => "None"
85 | Some x => "Some(" ^ show x ^ ")")
86 (* end *)
87
88 (* begin eval *)
89 predecessor 6
90 (* end *)
91
92 (* begin eval *)
93 predecessor 0
94 (* end *)