module HOL.Util
where
mkUnsafe :: String -> Maybe a -> a
mkUnsafe :: String -> Maybe a -> a
mkUnsafe String
_ (Just a
x) = a
x
mkUnsafe String
s Maybe a
Nothing = String -> a
forall a. HasCallStack => String -> a
error (String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" failed")
mkUnsafe1 :: String -> (a -> Maybe b) -> a -> b
mkUnsafe1 :: String -> (a -> Maybe b) -> a -> b
mkUnsafe1 String
s a -> Maybe b
f = String -> Maybe b -> b
forall a. String -> Maybe a -> a
mkUnsafe String
s (Maybe b -> b) -> (a -> Maybe b) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe b
f
mkUnsafe2 :: String -> (a -> b -> Maybe c) -> a -> b -> c
mkUnsafe2 :: String -> (a -> b -> Maybe c) -> a -> b -> c
mkUnsafe2 String
s a -> b -> Maybe c
f = String -> (b -> Maybe c) -> b -> c
forall a b. String -> (a -> Maybe b) -> a -> b
mkUnsafe1 String
s ((b -> Maybe c) -> b -> c) -> (a -> b -> Maybe c) -> a -> b -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b -> Maybe c
f