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.

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