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

Produced by Haddock version 2.4.2