src/HOL/MiniML/Maybe.thy
author nipkow
Mon, 03 Nov 1997 09:58:06 +0100
changeset 4072 d0d32dd77440
parent 3842 b55686a7b22c
child 12919 d6a0d168291e
permissions -rw-r--r--
expand_option_bind -> split_option_bind

(* Title:     HOL/MiniML/Maybe.thy
   ID:        $Id$
   Author:    Wolfgang Naraschewski and Tobias Nipkow
   Copyright  1996 TU Muenchen

Universal error monad.
*)

Maybe = Option + List +

constdefs
  option_bind :: ['a option, 'a => 'b option] => 'b option
  "option_bind m f == case m of None => None | Some r => f r"

syntax "@option_bind" :: [pttrns,'a option,'b] => 'c ("(_ := _;//_)" 0)
translations "P := E; F" == "option_bind E (%P. F)"

end