# HG changeset patch # User wenzelm # Date 932669578 -7200 # Node ID 69d42b56151fd073a30b9e6b6797682d1baf6777 # Parent 80d244f81b96501b6b48956184df4ee7e0f68a31 added exists; diff -r 80d244f81b96 -r 69d42b56151f src/Pure/General/table.ML --- a/src/Pure/General/table.ML Thu Jul 22 16:54:33 1999 +0200 +++ b/src/Pure/General/table.ML Thu Jul 22 20:52:58 1999 +0200 @@ -24,6 +24,7 @@ val foldl: ('a * (key * 'b) -> 'a) -> 'a * 'b table -> 'a val dest: 'a table -> (key * 'a) list val keys: 'a table -> key list + val exists: (key * 'a -> bool) -> 'a table -> bool val lookup: 'a table * key -> 'a option val update: (key * 'a) * 'a table -> 'a table val update_new: (key * 'a) * 'a table -> 'a table (*exception DUP*) @@ -76,6 +77,7 @@ fun dest tab = rev (foldl_table (fn (rev_ps, p) => p :: rev_ps) ([], tab)); fun keys tab = rev (foldl_table (fn (rev_ks, (k, _)) => k :: rev_ks) ([], tab)); +fun exists P tab = foldl_table (fn (false, e) => P e | (b, _) => b) (false, tab); (* lookup *)