src/HOL/MiniML/Maybe.thy
author clasohm
Wed, 06 Mar 1996 14:19:39 +0100
changeset 1557 fe30812f5b5e
parent 1400 5d909faf0e04
child 2525 477c05586286
permissions -rw-r--r--
added constdefs section
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$
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     3
   Author:    Dieter Nazareth and Tobias Nipkow
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     4
   Copyright  1995 TU Muenchen
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
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     9
Maybe = List +
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    10
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    11
datatype 'a maybe =  Ok 'a | Fail
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    12
1557
fe30812f5b5e added constdefs section
clasohm
parents: 1400
diff changeset
    13
constdefs
fe30812f5b5e added constdefs section
clasohm
parents: 1400
diff changeset
    14
  bind :: ['a maybe, 'a => 'b maybe] => 'b maybe (infixl 60)
fe30812f5b5e added constdefs section
clasohm
parents: 1400
diff changeset
    15
  "m bind f == case m of Ok r => f r | Fail => Fail"
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    16
1400
5d909faf0e04 Introduced Monad syntax Pat := Val; Cont
nipkow
parents: 1376
diff changeset
    17
syntax "@bind" :: [pttrns,'a maybe,'b] => 'c ("(_ := _;//_)" 0)
5d909faf0e04 Introduced Monad syntax Pat := Val; Cont
nipkow
parents: 1376
diff changeset
    18
translations "P := E; F" == "E bind (%P.F)"
5d909faf0e04 Introduced Monad syntax Pat := Val; Cont
nipkow
parents: 1376
diff changeset
    19
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    20
end