tuned signature: more operations;
authorwenzelm
Fri, 17 Jan 2025 11:49:31 +0100
changeset 81845 acd9849d4e9e
parent 81844 f9d0d2ca2402
child 81846 5a7bf0f038e2
tuned signature: more operations;
src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Fri Jan 17 11:47:47 2025 +0100
+++ b/src/Pure/General/path.ML	Fri Jan 17 11:49:31 2025 +0100
@@ -35,6 +35,8 @@
   val split_ext: T -> T * string
   val drop_ext: T -> T
   val get_ext: T -> string
+  val is_xz: T -> bool
+  val is_zst: T -> bool
   val expand: T -> T
   val file_name: T -> string
   eqtype binding
@@ -217,6 +219,9 @@
 val drop_ext = #1 o split_ext;
 val get_ext = #2 o split_ext;
 
+fun is_xz path = get_ext path = "xz";
+fun is_zst path = get_ext path = "zst";
+
 
 (* expand variables *)