Agda-2.3.0: 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 :: TermLike a => a -> TCM aSource

etaOnce :: Term -> TCM Term Source