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