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

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

3. checkTelePiSort :: Type -> TCM ()

   Agda	Agda.TypeChecking.Sort

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

4. hasBiggerSort :: Sort -> TCM ()

   Agda	Agda.TypeChecking.Sort

   No documentation available.

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

   Agda	Agda.TypeChecking.Sort

   No documentation available.

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

   Agda	Agda.TypeChecking.Sort

   No documentation available.

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

   Agda	Agda.TypeChecking.Sort

   As inferPiSort, but for a nondependent function type.

8. inferPiSort :: (PureTCM m, MonadConstraint m) => Dom Type -> Abs Sort -> m Sort

   Agda	Agda.TypeChecking.Sort

   Infer the sort of a Pi type. If we can compute the sort straight away, return that. Otherwise, return a PiSort and add a constraint to ensure we can compute the sort eventually.

9. inferUnivSort :: (PureTCM m, MonadConstraint m) => Sort -> m Sort

   Agda	Agda.TypeChecking.Sort

   Infer the sort of another sort. If we can compute the bigger sort straight away, return that. Otherwise, return UnivSort s and add a constraint to ensure we can compute the sort eventually.

10. shouldBeSort :: (PureTCM m, MonadBlock m, MonadError TCErr m) => Type -> m Sort

    Agda	Agda.TypeChecking.Sort

    Result is in reduced form.

Page 175 of many | Previous | Next