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

Agda.TypeChecking.EtaContract

Description

Compute eta short normal forms.

Documentation

data BinAppView Source

Constructors

App Term (Arg Term)
NoApp Term

binAppView :: Term -> BinAppView Source

etaContract :: (MonadTCM tcm, TermLike a) => a -> tcm aSource

etaOnce :: MonadTCM tcm => Term -> tcm Term Source