Hoogle Search

Within LTS Haskell 24.38 (ghc-9.10.3)

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

Exact lookup

1. equalityUnview :: EqualityUnview a => a -> Type

   Agda	Agda.TypeChecking.Monad.Builtin

   No documentation available.

2. equalityView :: Range -> Type -> TCM EqualityView

   Agda	Agda.TypeChecking.Monad.Builtin

   Check whether the type is actually an equality (lhs ≡ rhs) and extract lhs, rhs, and their type. Precondition: type is reduced.

3. equals :: Applicative m => m Doc

   Agda	Agda.TypeChecking.Pretty

   No documentation available.

4. eqFreeVars :: PostponedEquation -> Context

   Agda	Agda.TypeChecking.Rewriting.NonLinMatch

   Context of free variables in the equation

5. eqLhs :: PostponedEquation -> Term

   Agda	Agda.TypeChecking.Rewriting.NonLinMatch

   Term from pattern, living in pattern context.

6. eqRhs :: PostponedEquation -> Term

   Agda	Agda.TypeChecking.Rewriting.NonLinMatch

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

7. eqType :: PostponedEquation -> Type

   Agda	Agda.TypeChecking.Rewriting.NonLinMatch

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

8. 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)

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

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

   No documentation available.

10. eqCount :: UnifyState -> Int

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

    No documentation available.

Page 121 of many | Previous | Next