| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.EtaExpand
Description
Compute eta long normal forms.
Synopsis
- etaExpandOnce :: (MonadReduce m, MonadTCEnv m, HasOptions m, HasConstInfo m, MonadDebug m) => Type -> Term -> m Term
- deepEtaExpand :: Term -> Type -> TCM Term
- etaExpandAction :: (MonadReduce m, MonadTCEnv m, HasOptions m, HasConstInfo m, MonadDebug m) => Action m
Documentation
etaExpandOnce :: (MonadReduce m, MonadTCEnv m, HasOptions m, HasConstInfo m, MonadDebug m) => Type -> Term -> m Term Source #
Eta-expand a term if its type is a function type or an eta-record type.
deepEtaExpand :: Term -> Type -> TCM Term Source #
Eta-expand functions and expressions of eta-record type wherever possible.
etaExpandAction :: (MonadReduce m, MonadTCEnv m, HasOptions m, HasConstInfo m, MonadDebug m) => Action m Source #