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.
inferPiSort :: (PureTCM m, MonadConstraint m) => Dom Type -> Abs Sort -> m SortAgda Agda.TypeChecking.Sort Infer the sort of a Pi type. If we can compute the sort straight away, return that. Otherwise, return a PiSort and add a constraint to ensure we can compute the sort eventually.
inferUnivSort :: (PureTCM m, MonadConstraint m) => Sort -> m SortAgda Agda.TypeChecking.Sort Infer the sort of another sort. If we can compute the bigger sort straight away, return that. Otherwise, return UnivSort s and add a constraint to ensure we can compute the sort eventually.
shouldBeSort :: (PureTCM m, MonadBlock m, MonadError TCErr m) => Type -> m SortAgda Agda.TypeChecking.Sort Result is in reduced form.
pattern
LargeSort :: Univ -> Integer -> SizeOfSortAgda Agda.TypeChecking.Substitute No documentation available.
-
Agda Agda.TypeChecking.Substitute A sort can either be small (Set l, Prop l, Size, ...) or large (Setω n).
SizeOfSort :: Univ -> Integer -> SizeOfSortAgda Agda.TypeChecking.Substitute No documentation available.
pattern
SmallSort :: Univ -> SizeOfSortAgda Agda.TypeChecking.Substitute No documentation available.
funSort :: Sort -> Sort -> SortAgda Agda.TypeChecking.Substitute No documentation available.
funSort' :: Sort -> Sort -> Either Blocker SortAgda 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.
-
Agda Agda.TypeChecking.Substitute No documentation available.