{-# LANGUAGE OverloadedStrings #-} module Agda.Interaction.Command.RetryConstraints where import Agda.TypeChecking.Constraints (wakeupConstraints_) import Agda.TypeChecking.Monad.Base (TCM) import Data.ByteString (ByteString) retryConstraints :: TCM ByteString retryConstraints :: TCM ByteString retryConstraints = TCM () wakeupConstraints_ TCM () -> TCM ByteString -> TCM ByteString forall (m :: * -> *) a b. Monad m => m a -> m b -> m b >> ByteString -> TCM ByteString forall (f :: * -> *) a. Applicative f => a -> f a pure ByteString "Awaken."