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. relevantInIgnoringSortAnn :: Free t => Nat -> t -> Bool

   Agda	Agda.TypeChecking.Free

   No documentation available.

2. data IgnoreSorts

   Agda	Agda.TypeChecking.Free.Lazy

   Where should we skip sorts in free variable analysis?

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

   Agda	Agda.TypeChecking.Free.Lazy

   Ignore free variables in sorts.

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

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

   Agda	Agda.TypeChecking.MetaVars

   Sort metas in dependency order.

6. newSortMeta :: MonadMetaSolver m => m Sort

   Agda	Agda.TypeChecking.MetaVars

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

7. newSortMetaBelowInf :: TCM Sort

   Agda	Agda.TypeChecking.MetaVars

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

8. newSortMetaCtx :: MonadMetaSolver m => Args -> m Sort

   Agda	Agda.TypeChecking.MetaVars

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

9. data BuiltinSort

   Agda	Agda.TypeChecking.Monad.Base

   No documentation available.

10. BuiltinSort :: BuiltinSort -> BuiltinDescriptor

    Agda	Agda.TypeChecking.Monad.Base

    No documentation available.

Page 170 of many | Previous | Next