| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.EtaExpand
Description
Compute eta long normal forms.
Synopsis
- etaExpandOnce :: PureTCM m => Type -> Term -> m Term
- deepEtaExpand :: Term -> Type -> TCM Term
- etaExpandAction :: PureTCM m => Action m
Documentation
etaExpandOnce :: PureTCM 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 :: PureTCM m => Action m Source #