summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Thu, 11 Oct 2001 19:22:15 +0200 | |

changeset 11721 | 0d60622b668f |

parent 11720 | 5341e38309e8 |

child 11722 | 78cf55fd57c6 |

added try;

--- a/src/Pure/General/seq.ML Thu Oct 11 19:22:00 2001 +0200 +++ b/src/Pure/General/seq.ML Thu Oct 11 19:22:15 2001 +0200 @@ -17,6 +17,7 @@ val empty: 'a seq val cons: 'a * 'a seq -> 'a seq val single: 'a -> 'a seq + val try: ('a -> 'b) -> 'a -> 'b seq val hd: 'a seq -> 'a val tl: 'a seq -> 'a seq val chop: int * 'a seq -> 'a list * 'a seq @@ -73,6 +74,12 @@ fun hd xq = #1 (the (pull xq)) and tl xq = #2 (the (pull xq)); +(*partial function as procedure*) +fun try f x = + (case Library.try f x of + Some y => single y + | None => empty); + (*the list of the first n elements, paired with rest of sequence; if length of list is less than n, then sequence had less than n elements*)