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

Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.EtaExpand

Description

Compute eta long normal forms.

Synopsis

etaExpandOnce :: PureTCM m => Type -> Term -> m Term
deepEtaExpand :: Term -> Type -> TCM Term
etaExpandAction :: forall (m :: Type -> Type). PureTCM m => Action m

Documentation

etaExpandOnce :: PureTCM m => Type -> Term -> m Term Source #

Eta-expand a term if its type is a function type or an eta-record type.

deepEtaExpand :: Term -> Type -> TCM Term Source #

Eta-expand functions and expressions of eta-record type wherever possible.

etaExpandAction :: forall (m :: Type -> Type). PureTCM m => Action m Source #