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. leqSort :: MonadConversion m => Sort -> Sort -> m ()

   Agda	Agda.TypeChecking.Conversion

   Check that the first sort is less or equal to the second. We can put SizeUniv below Inf, but otherwise, it is unrelated to the other universes.

2. data IgnoreSorts

   Agda	Agda.TypeChecking.Free

   Where should we skip sorts in free variable analysis?

3. freeInIgnoringSorts :: Free a => Nat -> a -> Bool

   Agda	Agda.TypeChecking.Free

   No documentation available.

4. relevantInIgnoringSortAnn :: Free t => Nat -> t -> Bool

   Agda	Agda.TypeChecking.Free

   No documentation available.

5. data IgnoreSorts

   Agda	Agda.TypeChecking.Free.Lazy

   Where should we skip sorts in free variable analysis?

6. feIgnoreSorts :: FreeEnv' a IgnoreSorts c -> IgnoreSorts

   Agda	Agda.TypeChecking.Free.Lazy

   Ignore free variables in sorts.

7. isCoFibrantSort :: (LensSort a, PureTCM m) => a -> m (Either Blocker Bool)

   Agda	Agda.TypeChecking.Irrelevance

   Cofibrant types are those that could be the domain of a fibrant pi type. (Notion by C. Sattler).

8. dependencySortMetas :: [MetaId] -> TCM (Maybe [MetaId])

   Agda	Agda.TypeChecking.MetaVars

   Sort metas in dependency order.

9. newSortMeta :: MonadMetaSolver m => m Sort

   Agda	Agda.TypeChecking.MetaVars

   Create a sort meta that may be instantiated with Inf (Setω).

10. newSortMetaBelowInf :: TCM Sort

    Agda	Agda.TypeChecking.MetaVars

    Create a sort meta that cannot be instantiated with Inf (Setω).

Page 170 of many | Previous | Next