src/HOL/MiniML/Maybe.thy
author nipkow
Fri, 17 Jan 1997 18:32:24 +0100
changeset 2523 0ccea141409b
parent 1557 fe30812f5b5e
child 2525 477c05586286
permissions -rw-r--r--
Updated documentation pointers.

(* 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

constdefs
  bind :: ['a maybe, 'a => 'b maybe] => 'b maybe (infixl 60)
  "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