more Isabelle/Haskell operations;
authorwenzelm
Mon, 30 Aug 2021 21:45:05 +0200
changeset 74496 736374547a7f
parent 74495 a308ed696b58
child 74497 8798edfc61ef
more Isabelle/Haskell operations;
src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Mon Aug 30 21:41:37 2021 +0200
+++ b/src/Tools/Haskell/Haskell.thy	Mon Aug 30 21:45:05 2021 +0200
@@ -2161,7 +2161,7 @@
 module Isabelle.Name (
   Name,
   uu, uu_, aT,
-  clean_index, clean, internal, skolem, is_internal, is_skolem,
+  clean_index, clean, internal, skolem, is_internal, is_skolem, dest_internal, dest_skolem,
   Context, declare, is_declared, context, make_context, variant
 )
 where
@@ -2199,6 +2199,10 @@
 is_internal = Bytes.isSuffixOf "_"
 is_skolem = Bytes.isSuffixOf "__"
 
+dest_internal, dest_skolem :: Name -> Maybe Name
+dest_internal = Bytes.try_unsuffix "_"
+dest_skolem = Bytes.try_unsuffix "__"
+
 clean_index :: Name -> (Name, Int)
 clean_index x =
   if Bytes.null x || Bytes.last x /= underscore then (x, 0)