author | nipkow |
Fri, 08 Dec 1995 19:48:15 +0100 | |
changeset 1400 | 5d909faf0e04 |
parent 1376 | 92f83b9d17e1 |
child 1557 | fe30812f5b5e |
permissions | -rw-r--r-- |
(* Title: HOL/MiniML/Maybe.thy ID: $Id$ Author: Dieter Nazareth and Tobias Nipkow Copyright 1995 TU Muenchen Universal error monad. *) Maybe = List + datatype 'a maybe = Ok 'a | Fail consts bind :: ['a maybe, 'a => 'b maybe] => 'b maybe (infixl 60) defs bind_def "m bind f == case m of Ok r => f r | Fail => Fail" syntax "@bind" :: [pttrns,'a maybe,'b] => 'c ("(_ := _;//_)" 0) translations "P := E; F" == "E bind (%P.F)" end