Agda-2.2.6: 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 -> BinAppViewSource

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