ModuleAgda-2.7.0.1Haskell2010
Agda.TypeChecking.EtaContract
Compute eta short normal forms.
- 1 type
- 5 values
- PackageAgda-2.7.0.1
- Exports6
- LanguageHaskell2010
- LicenceMIT
- SourceEtaContract.hs
Contracts all eta-redexes it sees without reducing.
value
etaCon :: (MonadTCEnv m, HasConstInfo m, HasOptions m)=> ConHeadConstructor name
c.-> ConInfoConstructor info
ci.-> ElimsConstructor arguments
args.-> (QName -> ConHead -> ConInfo -> Args -> m Term)Eta-contraction workhorse, gets also name of record type.
-> m TermReturns
Con c ci argsor its eta-contraction.
If record constructor, call eta-contraction function.
value
etaLam :: (MonadTCEnv m, HasConstInfo m, HasOptions m)=> ArgInfoInfo
iof the Lam.-> ArgNameName
xof the abstraction.-> Term-> m TermLam i (Abs x b), eta-contracted if possible.
Try to contract a lambda-abstraction Lam i (Abs x b).