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. equalLevel :: MonadConversion m => Level -> Level -> m ()

   Agda	Agda.TypeChecking.Conversion

   No documentation available.

2. equalSort :: MonadConversion m => Sort -> Sort -> m ()

   Agda	Agda.TypeChecking.Conversion

   Check that the first sort equal to the second.

3. equalTerm :: MonadConversion m => Type -> Term -> Term -> m ()

   Agda	Agda.TypeChecking.Conversion

   No documentation available.

4. equalTermOnFace :: MonadConversion m => Term -> Type -> Term -> Term -> m ()

   Agda	Agda.TypeChecking.Conversion

   equalTermOnFace φ A u v = _ , φ ⊢ u = v : A

5. equalType :: MonadConversion m => Type -> Type -> m ()

   Agda	Agda.TypeChecking.Conversion

   No documentation available.

6. eQuantity :: Lens' TCEnv Quantity

   Agda	Agda.TypeChecking.Monad.Base

   Note that this lens does not satisfy all lens laws: If hard compile-time mode is enabled, then quantities other than zero are replaced by __IMPOSSIBLE__.

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

   Agda	Agda.TypeChecking.Monad.Builtin

   No documentation available.

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

9. equals :: Applicative m => m Doc

   Agda	Agda.TypeChecking.Pretty

   No documentation available.

10. eqFreeVars :: PostponedEquation -> Context

    Agda	Agda.TypeChecking.Rewriting.NonLinMatch

    Context of free variables in the equation

Page 120 of many | Previous | Next