| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Agda.TypeChecking.EtaContract
Description
Compute eta short normal forms.
- data BinAppView
- binAppView :: Term -> BinAppView
- etaContract :: TermLike a => a -> TCM a
- etaOnce :: (MonadReader TCEnv m, HasConstInfo m) => Term -> m Term
Documentation
binAppView :: Term -> BinAppView Source
etaContract :: TermLike a => a -> TCM a Source
Contracts all eta-redexes it sees without reducing.
etaOnce :: (MonadReader TCEnv m, HasConstInfo m) => Term -> m Term Source