Hoogle Search
Within LTS Haskell 24.32 (ghc-9.10.3)
Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.
nlpTypeSort :: NLPType -> NLPSortAgda Agda.TypeChecking.Monad.Base No documentation available.
primSortName :: Defn -> BuiltinSortAgda Agda.TypeChecking.Monad.Base No documentation available.
-
Agda Agda.TypeChecking.Monad.Base No documentation available.
infallibleSortKit :: HasBuiltins m => m SortKitAgda Agda.TypeChecking.Monad.Builtin Compute a SortKit in contexts that do not support failure (e.g. Reify). This should only be used when we are sure that the primitive sorts have been bound, i.e. because it is "after" type checking.
-
Agda Agda.TypeChecking.Monad.Builtin No documentation available.
mkSortKit :: QName -> QName -> QName -> QName -> QName -> QName -> SortKitAgda Agda.TypeChecking.Monad.Builtin No documentation available.
primAgdaSort :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m TermAgda Agda.TypeChecking.Monad.Builtin No documentation available.
primAgdaSortInf :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m TermAgda Agda.TypeChecking.Monad.Builtin No documentation available.
primAgdaSortLit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m TermAgda Agda.TypeChecking.Monad.Builtin No documentation available.
primAgdaSortProp :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m TermAgda Agda.TypeChecking.Monad.Builtin No documentation available.