src/HOL/W0/Maybe.thy
author oheimb
Fri, 20 Feb 1998 16:00:18 +0100
changeset 4637 bac998af6ea2
parent 3842 b55686a7b22c
permissions -rw-r--r--
extended input syntax to handle names of special keys
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2520
aecaa76e7eff Incorporated Larry's changes.
nipkow
parents: 2518
diff changeset
     1
(* Title:     HOL/W0/Maybe.thy
2518
bee082efaa46 This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff changeset
     2
   ID:        $Id$
bee082efaa46 This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff changeset
     3
   Author:    Dieter Nazareth and Tobias Nipkow
bee082efaa46 This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff changeset
     4
   Copyright  1995 TU Muenchen
bee082efaa46 This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff changeset
     5
bee082efaa46 This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff changeset
     6
Universal error monad.
bee082efaa46 This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff changeset
     7
*)
bee082efaa46 This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff changeset
     8
bee082efaa46 This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff changeset
     9
Maybe = List +
bee082efaa46 This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff changeset
    10
bee082efaa46 This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff changeset
    11
datatype 'a maybe =  Ok 'a | Fail
bee082efaa46 This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff changeset
    12
bee082efaa46 This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff changeset
    13
constdefs
bee082efaa46 This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff changeset
    14
  bind :: ['a maybe, 'a => 'b maybe] => 'b maybe (infixl 60)
bee082efaa46 This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff changeset
    15
  "m bind f == case m of Ok r => f r | Fail => Fail"
bee082efaa46 This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff changeset
    16
3692
9f9bcce140ce tuned pattern syntax;
wenzelm
parents: 2520
diff changeset
    17
syntax "@bind" :: [patterns,'a maybe,'b] => 'c ("(_ := _;//_)" 0)
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3692
diff changeset
    18
translations "P := E; F" == "E bind (%P. F)"
2518
bee082efaa46 This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff changeset
    19
bee082efaa46 This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff changeset
    20
end