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

2. ssort :: Level -> Type

   Agda	Agda.TypeChecking.Substitute

   No documentation available.

3. szSortSize :: SizeOfSort -> Integer

   Agda	Agda.TypeChecking.Substitute

   No documentation available.

4. szSortUniv :: SizeOfSort -> Univ

   Agda	Agda.TypeChecking.Substitute

   No documentation available.

5. univSort :: Sort -> Sort

   Agda	Agda.TypeChecking.Substitute

   No documentation available.

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

7. module Agda.Utils.Graph.TopSort

   No documentation available.

8. topSort :: Ord n => Set n -> [(n, n)] -> Maybe [n]

   Agda	Agda.Utils.Graph.TopSort

   topoligical sort with smallest-numbered available vertex first | input: nodes, edges | output is Nothing if the graph is not a DAG Note: should be stable to preserve order of generalizable variables. Algorithm due to Richard Eisenberg, and works by walking over the list left-to-right and moving each node the minimum distance left to guarantee topological ordering.

9. topoSort :: (a -> a -> Bool) -> [a] -> Maybe Permutation

   Agda	Agda.Utils.Permutation

   Stable topologic sort. The first argument decides whether its first argument is an immediate parent to its second argument.

10. topoSortM :: Monad m => (a -> a -> m Bool) -> [a] -> m (Maybe Permutation)

    Agda	Agda.Utils.Permutation

    No documentation available.

Page 177 of many | Previous | Next