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.

Exact lookup

1. primAgdaSortPropLit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

   Agda	Agda.TypeChecking.Monad.Builtin

   No documentation available.

2. primAgdaSortSet :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

   Agda	Agda.TypeChecking.Monad.Builtin

   No documentation available.

3. primAgdaSortUnsupported :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

   Agda	Agda.TypeChecking.Monad.Builtin

   No documentation available.

4. primAgdaTermSort :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

   Agda	Agda.TypeChecking.Monad.Builtin

   No documentation available.

5. isSortJudgement :: Judgement a -> Bool

   Agda	Agda.TypeChecking.Monad.MetaVars

   No documentation available.

6. isSortMeta :: ReadTCState m => MetaId -> m Bool

   Agda	Agda.TypeChecking.Monad.MetaVars

   No documentation available.

7. isSortMeta_ :: MetaVariable -> Bool

   Agda	Agda.TypeChecking.Monad.MetaVars

   No documentation available.

8. sizeSort :: Sort

   Agda	Agda.TypeChecking.Monad.SizedTypes

   The sort of built-in types SIZE and SIZELT.

9. checkDataSort :: QName -> Sort -> TCM ()

   Agda	Agda.TypeChecking.Rules.Data

   Make sure that the target universe admits data type definitions. E.g. IUniv, SizeUniv etc. do not accept new constructions.

10. checkIndexSorts :: Sort -> Telescope -> TCM ()

    Agda	Agda.TypeChecking.Rules.Data

    When --without-K is enabled, we should check that the sorts of the index types fit into the sort of the datatype.

Page 174 of many | Previous | Next