Agda-2.2.10: A dependently typed functional programming language and proof assistant
Source code
Contents
Index
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 a
Source
etaOnce
::
MonadTCM
tcm =>
Term
-> tcm
Term
Source
Produced by
Haddock
version 2.6.1