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

Safe HaskellNone

Agda.TypeChecking.EtaContract

Description

Compute eta short normal forms.

Documentation

data BinAppView

Constructors

App Term (Arg Term) 
NoApp Term 

etaContract :: TermLike a => a -> TCM a