| author | paulson |
| Wed, 05 Nov 1997 13:23:46 +0100 | |
| changeset 4153 | e534c4c32d54 |
| parent 4133 | 0a08c2b9b1ed |
| child 4192 | c38ab5af38b5 |
| permissions | -rw-r--r-- |
| 2019 | 1 |
(* Title: Option.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1994 TU Muenchen |
|
5 |
||
6 |
Datatype 'a option |
|
7 |
*) |
|
8 |
||
9 |
Option = Arith + |
|
| 4133 | 10 |
|
| 2019 | 11 |
datatype 'a option = None | Some 'a |
| 4133 | 12 |
|
13 |
constdefs |
|
14 |
||
15 |
the :: "'a option => 'a" |
|
16 |
"the Ú %y. case y of None => arbitrary | Some x => x" |
|
17 |
||
18 |
option_map :: "('a => 'b) => ('a option => 'b option)"
|
|
19 |
"option_map Ú %f y. case y of None => None | Some x => Some (f x)" |
|
20 |
||
| 2019 | 21 |
end |