Hoogle Search

Within LTS Haskell 24.6 (ghc-9.10.2)

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

Exact lookup

1. eqLhs :: PostponedEquation -> Term

   Agda	Agda.TypeChecking.Rewriting.NonLinMatch

   Term from pattern, living in pattern context.

2. eqRhs :: PostponedEquation -> Term

   Agda	Agda.TypeChecking.Rewriting.NonLinMatch

   Term from scrutinee, living in context where matching was invoked.

3. eqType :: PostponedEquation -> Type

   Agda	Agda.TypeChecking.Rewriting.NonLinMatch

   Type of the equation, living in same context as the rhs.

4. equal :: PureTCM m => Type -> Term -> Term -> m (Maybe Blocked_)

   Agda	Agda.TypeChecking.Rewriting.NonLinMatch

   Typed βη-equality, also handles empty record types. Returns Nothing if the terms are equal, or `Just b` if the terms are not (where b contains information about possible metas blocking the comparison)

5. eqConstructorForm :: HasBuiltins m => Equality -> m Equality

   Agda	Agda.TypeChecking.Rules.LHS.Unify.Types

   No documentation available.

6. eqCount :: UnifyState -> Int

   Agda	Agda.TypeChecking.Rules.LHS.Unify.Types

   No documentation available.

7. eqLHS :: UnifyState -> [Arg Term]

   Agda	Agda.TypeChecking.Rules.LHS.Unify.Types

   Ends up in dot patterns (should not be reduced eagerly).

8. eqRHS :: UnifyState -> [Arg Term]

   Agda	Agda.TypeChecking.Rules.LHS.Unify.Types

   Ends up in dot patterns (should not be reduced eagerly).

9. eqTel :: UnifyState -> Telescope

   Agda	Agda.TypeChecking.Rules.LHS.Unify.Types

   Can be reduced eagerly.

10. eqUnLevel :: (HasBuiltins m, HasOptions m) => Equality -> m Equality

    Agda	Agda.TypeChecking.Rules.LHS.Unify.Types

    No documentation available.

Page 121 of many | Previous | Next