src/Pure/General/basics.ML
changeset 22935 c6689e15bc98
parent 21394 9f20604d2b5e
child 22936 284b56463da8
equal deleted inserted replaced
22934:64ecb3d6790a 22935:c6689e15bc98
    21   val #>> : ('a -> 'c * 'b) * ('c -> 'd) -> 'a -> 'd * 'b
    21   val #>> : ('a -> 'c * 'b) * ('c -> 'd) -> 'a -> 'd * 'b
    22   val ##> : ('a -> 'c * 'b) * ('b -> 'd) -> 'a -> 'c * 'd
    22   val ##> : ('a -> 'c * 'b) * ('b -> 'd) -> 'a -> 'c * 'd
    23   val ##>> : ('a -> 'c * 'b) * ('b -> 'e * 'd) -> 'a -> ('c * 'e) * 'd
    23   val ##>> : ('a -> 'c * 'b) * ('b -> 'e * 'd) -> 'a -> ('c * 'e) * 'd
    24   val ` : ('b -> 'a) -> 'b -> 'a * 'b
    24   val ` : ('b -> 'a) -> 'b -> 'a * 'b
    25   val tap: ('b -> 'a) -> 'b -> 'b
    25   val tap: ('b -> 'a) -> 'b -> 'b
       
    26   val flip: ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
    26 
    27 
    27   (*options*)
    28   (*options*)
    28   val is_some: 'a option -> bool
    29   val is_some: 'a option -> bool
    29   val is_none: 'a option -> bool
    30   val is_none: 'a option -> bool
    30   val the: 'a option -> 'a
    31   val the: 'a option -> 'a
    69 
    70 
    70 (*result views*)
    71 (*result views*)
    71 fun `f = fn x => (f x, x);
    72 fun `f = fn x => (f x, x);
    72 fun tap f = fn x => (f x; x);
    73 fun tap f = fn x => (f x; x);
    73 
    74 
       
    75 fun flip f x y = f y x
    74 
    76 
    75 (* options *)
    77 (* options *)
    76 
    78 
    77 fun is_some (SOME _) = true
    79 fun is_some (SOME _) = true
    78   | is_some NONE = false;
    80   | is_some NONE = false;