# HG changeset patch
# User wenzelm
# Date 1630009535 -7200
# Node ID c832f35ea57158c6cc9b024bb9d58ac6985b1e5d
# Parent  92f08f3d77bdffffe2cccc0bb11e611544e89220
more Isabelle/Haskell operations;

diff -r 92f08f3d77bd -r c832f35ea571 src/Tools/Haskell/Haskell.thy
--- 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