comparison doc/intro.ur @ 1499:92c929793d0f

Preserve tutorial indentation
author Adam Chlipala <adam@chlipala.net>
date Fri, 15 Jul 2011 19:00:59 -0400
parents 8c32c7191bf0
children 483cc0602565
comparison
equal deleted inserted replaced
1498:8c32c7191bf0 1499:92c929793d0f
72 72
73 (* begin eval *) 73 (* begin eval *)
74 compose inc inc 3 74 compose inc inc 3
75 (* end *) 75 (* end *)
76 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. *) 77 (* 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. *)
78 78
79 fun predecessor (n : int) : option int = if n >= 1 then Some (n - 1) else None 79 fun predecessor (n : int) : option int = if n >= 1 then Some (n - 1) else None
80 80
81 (* begin hide *) 81 (* begin hide *)
82 fun show_option [t] (_ : show t) : show (option t) = 82 fun show_option [t] (_ : show t) : show (option t) =
90 (* end *) 90 (* end *)
91 91
92 (* begin eval *) 92 (* begin eval *)
93 predecessor 0 93 predecessor 0
94 (* end *) 94 (* end *)
95
96 (* Naturally, there are lists, too! *)
97
98 val numbers : list int = 1 :: 2 :: 3 :: []
99 val strings : list string = "a" :: "bc" :: []
100
101 fun length [a] (ls : list a) : int =
102 case ls of
103 [] => 0
104 | _ :: ls' => 1 + length ls'
105
106 (* begin eval *)
107 length numbers
108 (* end *)
109
110 (* begin eval *)
111 length strings
112 (* end *)