Safe Haskell | None |
---|
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 -> BinAppViewSource
etaContract :: TermLike a => a -> TCM aSource
Contracts all eta-redexes it sees without reducing.
etaOnce :: (MonadReader TCEnv m, HasConstInfo m) => Term -> m TermSource