Hoogle Search

Within LTS Haskell 24.33 (ghc-9.10.3)

Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.

  1. sizeSort :: Sort

    Agda Agda.TypeChecking.Monad.SizedTypes

    The sort of built-in types SIZE and SIZELT.

  2. 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.

  3. 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.

  4. forceSort :: Type -> TCM Sort

    Agda Agda.TypeChecking.Rules.Data

    Ensure that the type is a sort. If it is not directly a sort, compare it to a newSortMetaBelowInf.

  5. checkSortOfSplitVar :: (MonadTCM m, PureTCM m, MonadError TCErr m, LensSort a, PrettyTCM a, LensSort ty, PrettyTCM ty) => DataOrRecord -> a -> Telescope -> Maybe ty -> m ()

    Agda Agda.TypeChecking.Rules.LHS

    No documentation available.

  6. checkTelePiSort :: Type -> TCM ()

    Agda Agda.TypeChecking.Sort

    Recursively check that an iterated function type constructed by telePi is well-sorted.

  7. hasBiggerSort :: Sort -> TCM ()

    Agda Agda.TypeChecking.Sort

    No documentation available.

  8. ifIsSort :: (MonadReduce m, MonadBlock m) => Type -> (Sort -> m a) -> m a -> m a

    Agda Agda.TypeChecking.Sort

    No documentation available.

  9. ifNotSort :: (MonadReduce m, MonadBlock m) => Type -> m a -> (Sort -> m a) -> m a

    Agda Agda.TypeChecking.Sort

    No documentation available.

  10. inferFunSort :: (PureTCM m, MonadConstraint m) => Dom Type -> Sort -> m Sort

    Agda Agda.TypeChecking.Sort

    As inferPiSort, but for a nondependent function type.

Page 175 of many | Previous | Next