src/HOL/MiniML/Maybe.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 3842 b55686a7b22c
child 12919 d6a0d168291e
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     1
(* Title:     HOL/MiniML/Maybe.thy
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     2
   ID:        $Id$
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1557
diff changeset
     3
   Author:    Wolfgang Naraschewski and Tobias Nipkow
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1557
diff changeset
     4
   Copyright  1996 TU Muenchen
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     5
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     6
Universal error monad.
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     7
*)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     8
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1557
diff changeset
     9
Maybe = Option + List +
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    10
1557
fe30812f5b5e added constdefs section
clasohm
parents: 1400
diff changeset
    11
constdefs
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1557
diff changeset
    12
  option_bind :: ['a option, 'a => 'b option] => 'b option
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1557
diff changeset
    13
  "option_bind m f == case m of None => None | Some r => f r"
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    14
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1557
diff changeset
    15
syntax "@option_bind" :: [pttrns,'a option,'b] => 'c ("(_ := _;//_)" 0)
3842
b55686a7b22c fixed dots;
wenzelm
parents: 2525
diff changeset
    16
translations "P := E; F" == "option_bind E (%P. F)"
1400
5d909faf0e04 Introduced Monad syntax Pat := Val; Cont
nipkow
parents: 1376
diff changeset
    17
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    18
end