Agda.TypeChecking.EtaContract

Compute eta short normal forms.

Documentation

data BinAppView

Constructors

App Term (Arg Term)

NoApp Term

binAppView :: Term -> BinAppView

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

Contracts all eta-redexes it sees without reducing.

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

etaCon

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

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).