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. module Agda.TypeChecking.Rules.LHS.Problem

   No documentation available.

2. data Problem a

   Agda	Agda.TypeChecking.Rules.LHS.Problem

   The user patterns we still have to split on.

3. Problem :: [ProblemEq] -> [NamedArg Pattern] -> (LHSState a -> TCM a) -> Problem a

   Agda	Agda.TypeChecking.Rules.LHS.Problem

   No documentation available.

4. data ProblemEq

   Agda	Agda.TypeChecking.Rules.LHS.Problem

   A user pattern together with an internal term that it should be equal to after splitting is complete. Special cases: * User pattern is a variable but internal term isn't: this will be turned into an as pattern. * User pattern is a dot pattern: this pattern won't trigger any splitting but will be checked for equality after all splitting is complete and as patterns have been bound. * User pattern is an absurd pattern: emptiness of the type will be checked after splitting is complete. * User pattern is an annotated wildcard: type annotation will be checked after splitting is complete.

5. ProblemEq :: Pattern -> Term -> Dom Type -> ProblemEq

   Agda	Agda.TypeChecking.Rules.LHS.Problem

   No documentation available.

6. module Agda.TypeChecking.Rules.LHS.ProblemRest

   No documentation available.

7. PiNotLam :: LamOrPi

   Agda	Agda.TypeChecking.Rules.Term

   We are checking a telescope in a Pi-type. We stay in the term world, but add resurrected domains to the context to check the remaining domains and codomain of the Pi-type.

8. module Agda.TypeChecking.SizedTypes.Pretty

   No documentation available.

9. type Polarities flex = Map flex Polarity

   Agda	Agda.TypeChecking.SizedTypes.Syntax

   Type of solution wanted for each flexible.

10. data Polarity

    Agda	Agda.TypeChecking.SizedTypes.Syntax

    What type of solution are we looking for?

Page 1147 of many | Previous | Next