Searched refs:TCMT (Results 1 – 9 of 9) sorted by relevance
27 newtype TCMT m a = TCM { unTCM :: IORef TCState -> TCEnv -> m a }29 instance MonadIO m => Applicative (TCMT m)30 instance MonadIO m => Functor (TCMT m)31 instance MonadIO m => Monad (TCMT m)32 instance MonadIO m => MonadIO (TCMT m)34 type TCM = TCMT IO
10 import Agda.TypeChecking.Monad.Base (TCMT, Builtin, PrimFun)24 instance MonadIO m => HasBuiltins (TCMT m)
4173 type TCM = TCMT IO4176 mapTCMT :: (forall a. m a -> n a) -> TCMT m a -> TCMT n a4194 returnTCMT :: MonadIO m => a -> TCMT m a4198 bindTCMT :: MonadIO m => TCMT m a -> (a -> TCMT m b) -> TCMT m b4202 thenTCMT :: MonadIO m => TCMT m a -> TCMT m b -> TCMT m b4206 instance MonadIO m => Functor (TCMT m) where4209 fmapTCMT :: MonadIO m => (a -> b) -> TCMT m a -> TCMT m b4217 apTCMT :: MonadIO m => TCMT m (a -> b) -> TCMT m a -> TCMT m b4221 instance MonadTrans TCMT where4225 instance MonadIO m => Monad (TCMT m) where[all …]
54 instance MonadIO m => HasBuiltins (TCMT m) where
741 instance HasConstInfo (TCMT IO) where
17 , TCM, TCMT(..)31 newtype IM a = IM {unIM :: TCMT (Haskeline.InputT IO) a}
105 isVar :: Term -> TCMT IO (Maybe Int)
584 newtype RecPatM a = RecPatM (TCMT (ReaderT Nat (StateT Nat IO)) a)
139 …LIX8ufXe3n\n3aXNit7PiQoAbEFpUrIJyG/kETUEJe492mi+/PEXWLttEUwGmTqhTcKYCKrB+0TCMT/XI/Y9hRFQ\nBgpbWFwQ…