author | oheimb |
Tue, 04 Nov 1997 20:48:38 +0100 | |
changeset 4133 | 0a08c2b9b1ed |
parent 2019 | b45d9f2042e0 |
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 |