Agda-2.5.3: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.EtaContract

Description

Compute eta short normal forms.

Synopsis

Documentation

data BinAppView Source #

Constructors

App Term (Arg Term) 
NoApp Term 

etaContract :: (MonadReader TCEnv m, HasConstInfo m, HasOptions m, TermLike a) => a -> m a Source #

Contracts all eta-redexes it sees without reducing.