--- a/src/Tools/Haskell/Haskell.thy Thu Aug 26 22:15:55 2021 +0200
+++ b/src/Tools/Haskell/Haskell.thy Thu Aug 26 22:25:35 2021 +0200
@@ -222,7 +222,7 @@
module Isabelle.Library (
(|>), (|->), (#>), (#->),
- fold, fold_rev, single, the_single, map_index, get_index, separate,
+ fold, fold_rev, single, the_single, singletonM, map_index, get_index, separate,
StringLike, STRING (..), TEXT (..), BYTES (..),
show_bytes, show_text,
@@ -274,6 +274,9 @@
the_single [x] = x
the_single _ = undefined
+singletonM :: Monad m => ([a] -> m [b]) -> a -> m b
+singletonM f x = the_single <$> f [x]
+
map_index :: ((Int, a) -> b) -> [a] -> [b]
map_index f = map_aux 0
where