Agda-2.6.3.20230930: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.EtaContract

Description

Compute eta short normal forms.

Synopsis

Documentation

data BinAppView Source #

Constructors

App Term (Arg Term) 
NoApp Term 

binAppView :: Term -> BinAppView Source #

etaContract :: (MonadTCEnv m, HasConstInfo m, HasOptions m, TermLike a) => a -> m a Source #

Contracts all eta-redexes it sees without reducing.

etaOnce :: (MonadTCEnv m, HasConstInfo m, HasOptions m) => Term -> m Term Source #

etaCon Source #

Arguments

:: (MonadTCEnv m, HasConstInfo m, HasOptions m) 
=> ConHead

Constructor name c.

-> ConInfo

Constructor info ci.

-> Elims

Constructor arguments args.

-> (QName -> ConHead -> ConInfo -> Args -> m Term)

Eta-contraction workhorse, gets also name of record type.

-> m Term

Returns Con c ci args or its eta-contraction.

If record constructor, call eta-contraction function.

etaLam Source #

Arguments

:: (MonadTCEnv m, HasConstInfo m, HasOptions m) 
=> ArgInfo

Info i of the Lam.

-> ArgName

Name x of the abstraction.

-> Term

Body (Term) b of the Abs.

-> m Term

Lam i (Abs x b), eta-contracted if possible.

Try to contract a lambda-abstraction Lam i (Abs x b).