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. pattern LargeSort :: Univ -> Integer -> SizeOfSort

   Agda	Agda.TypeChecking.Substitute

   No documentation available.

2. data SizeOfSort

   Agda	Agda.TypeChecking.Substitute

   A sort can either be small (Set l, Prop l, Size, ...) or large (Setω n).

3. SizeOfSort :: Univ -> Integer -> SizeOfSort

   Agda	Agda.TypeChecking.Substitute

   No documentation available.

4. pattern SmallSort :: Univ -> SizeOfSort

   Agda	Agda.TypeChecking.Substitute

   No documentation available.

5. funSort :: Sort -> Sort -> Sort

   Agda	Agda.TypeChecking.Substitute

   No documentation available.

6. funSort' :: Sort -> Sort -> Either Blocker Sort

   Agda	Agda.TypeChecking.Substitute

   Compute the sort of a function type from the sorts of its domain and codomain. This function should only be called on reduced sorts, since the LevelUniv rules should only apply when the sort does not reduce to Set.

7. isSmallSort :: Sort -> Bool

   Agda	Agda.TypeChecking.Substitute

   No documentation available.

8. mkPiSort :: Dom Type -> Abs Type -> Sort

   Agda	Agda.TypeChecking.Substitute

   No documentation available.

9. piSort :: Dom Term -> Sort -> Abs Sort -> Sort

   Agda	Agda.TypeChecking.Substitute

   No documentation available.

10. piSort' :: Dom Term -> Sort -> Abs Sort -> Either Blocker Sort

    Agda	Agda.TypeChecking.Substitute

    Compute the sort of a pi type from the sorts of its domain and codomain. This function should only be called on reduced sorts, since the LevelUniv rules should only apply when the sort doesn't reduce to Set

Page 176 of many | Previous | Next