Hoogle Search

Within LTS Haskell 24.52 (ghc-9.10.3)

Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.

Exact lookup

1. data ProjEliminator

   Agda	Agda.TypeChecking.ProjectionLike

   No documentation available.

2. data ProjectionView

   Agda	Agda.TypeChecking.ProjectionLike

   View for a Def f (Apply a : es) where isRelevantProjection f. Used for projection-like fs.

3. ProjectionView :: QName -> Arg Term -> Elims -> ProjectionView

   Agda	Agda.TypeChecking.ProjectionLike

   A projection or projection-like function, applied to its principal argument

4. ProjT :: Dom Type -> Type -> ElimType

   Agda	Agda.TypeChecking.Records

   No documentation available.

5. data PostponedEquation

   Agda	Agda.TypeChecking.Rewriting.NonLinMatch

   Matching against a term produces a constraint which we have to verify after applying the substitution computed by matching.

6. PostponedEquation :: Context -> Type -> Term -> Term -> PostponedEquation

   Agda	Agda.TypeChecking.Rewriting.NonLinMatch

   No documentation available.

7. type PostponedEquations = [PostponedEquation]

   Agda	Agda.TypeChecking.Rewriting.NonLinMatch

   No documentation available.

8. class PatternFrom a b

   Agda	Agda.TypeChecking.Rewriting.NonLinPattern

   Turn a term into a non-linear pattern, treating the free variables as pattern variables. The first argument indicates the relevance we are working under: if this is Irrelevant, then we construct a pattern that never fails to match. The second argument is the number of bound variables (from pattern lambdas). The third argument is the type of the term.

9. PathCons :: IsPathCons

   Agda	Agda.TypeChecking.Rules.Data

   No documentation available.

10. PointCons :: IsPathCons

    Agda	Agda.TypeChecking.Rules.Data

    No documentation available.

Page 1146 of many | Previous | Next