Hoogle Search
Within LTS Haskell 24.4 (ghc-9.10.2)
Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.
-
Agda Agda.Syntax.Internal No documentation available.
-
Agda Agda.Syntax.Reflected No documentation available.
-
Agda Agda.Syntax.Reflected No documentation available.
-
This module contains the rules for Agda's sort system viewed as a pure type system (pts). The specification of a pts consists of a set of axioms of the form s1 : s2 specifying when a sort fits in another sort, and a set of rules of the form (s1,s2,s3) specifying that a pi type with domain in s1 and codomain in s2 itself fits into sort s3. To ensure unique principal types, the axioms and rules of Agda's pts are given by two partial functions univSort' and piSort' (see Agda.TypeChecking.Substitute). If these functions return Nothing, a constraint is added to ensure that the sort will be computed eventually. One upgrade over the standard definition of a pts is that in a rule (s1,s2,s3), in Agda the sort s2 can depend on a variable of some type in s1. This is needed to support Agda's universe polymorphism where we can have e.g. a function of type ∀ {ℓ} → Set ℓ.
-
bloodhound Database.Bloodhound.Common.Types Sort is a synonym for a list of SortSpecs. Sort behavior is order dependent with later sorts acting as tie-breakers for earlier sorts.
-
discrimination Data.Discrimination Stable Ordered Discriminator
Sort :: (forall b . () => [(a, b)] -> [[b]]) -> Sort adiscrimination Data.Discrimination No documentation available.
-
discrimination Data.Discrimination.Sorting Stable Ordered Discriminator
Sort :: (forall b . () => [(a, b)] -> [[b]]) -> Sort adiscrimination Data.Discrimination.Sorting No documentation available.
module Yi.Keymap.Vim.Ex.Commands.
Sort No documentation available.