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.

Exact lookup

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

   Agda	Agda.TypeChecking.Substitute

   No documentation available.

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

   Agda	Agda.TypeChecking.Substitute

   No documentation available.

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

4. sizeOfSort :: Sort -> Either Blocker SizeOfSort

   Agda	Agda.TypeChecking.Substitute

   Returns Left blocker for unknown (blocked) sorts, and otherwise returns Right s where s indicates the size and fibrancy.

5. ssort :: Level -> Type

   Agda	Agda.TypeChecking.Substitute

   No documentation available.

6. szSortSize :: SizeOfSort -> Integer

   Agda	Agda.TypeChecking.Substitute

   No documentation available.

7. szSortUniv :: SizeOfSort -> Univ

   Agda	Agda.TypeChecking.Substitute

   No documentation available.

8. univSort :: Sort -> Sort

   Agda	Agda.TypeChecking.Substitute

   No documentation available.

9. univSort' :: Sort -> Either Blocker Sort

   Agda	Agda.TypeChecking.Substitute

   univSort' univInf s gets the next higher sort of s, if it is known (i.e. it is not just UnivSort s). Precondition: s is reduced

10. module Agda.Utils.Graph.TopSort

    No documentation available.

Page 177 of many | Previous | Next