# HG changeset patch
# User wenzelm
# Date 1681202672 -7200
# Node ID aa814dc5a685a4619c958c5b1edd17760876801b
# Parent  c3330a54b9e59449619691b86eabec88c8c3198f
more operations;

diff -r c3330a54b9e5 -r aa814dc5a685 src/Pure/General/set.ML
--- a/src/Pure/General/set.ML	Tue Apr 11 09:54:46 2023 +0200
+++ b/src/Pure/General/set.ML	Tue Apr 11 10:44:32 2023 +0200
@@ -16,6 +16,8 @@
   val fold: (elem -> 'a -> 'a) -> T -> 'a -> 'a
   val fold_rev: (elem -> 'a -> 'a) -> T -> 'a -> 'a
   val dest: T -> elem list
+  val min: T -> elem option
+  val max: T -> elem option
   val exists: (elem -> bool) -> T -> bool
   val forall: (elem -> bool) -> T -> bool
   val get_first: (elem -> 'a option) -> T -> 'a option
@@ -152,6 +154,29 @@
 val dest = Library.build o fold_rev_set cons;
 
 
+(* min/max entries *)
+
+fun min Empty = NONE
+  | min (Leaf1 e) = SOME e
+  | min (Leaf2 (e, _)) = SOME e
+  | min (Leaf3 (e, _, _)) = SOME e
+  | min (Branch2 (Empty, e, _)) = SOME e
+  | min (Branch3 (Empty, e, _, _, _)) = SOME e
+  | min (Branch2 (left, _, _)) = min left
+  | min (Branch3 (left, _, _, _, _)) = min left
+  | min (Size (_, arg)) = min arg;
+
+fun max Empty = NONE
+  | max (Leaf1 e) = SOME e
+  | max (Leaf2 (_, e)) = SOME e
+  | max (Leaf3 (_, _, e)) = SOME e
+  | max (Branch2 (_, e, Empty)) = SOME e
+  | max (Branch3 (_, _, _, e, Empty)) = SOME e
+  | max (Branch2 (_, _, right)) = max right
+  | max (Branch3 (_, _, _, _, right)) = max right
+  | max (Size (_, arg)) = max arg;
+
+
 (* exists and forall *)
 
 fun exists pred =