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

Agda.TypeChecking.ReconstructParameters

Description

Reconstruct dropped parameters from constructors. Used by with-abstraction to avoid ill-typed abstractions (#745). Note that the term is invalid after parameter reconstruction. Parameters need to be dropped again before using it.

Documentation

reconstructParametersInType :: Type -> TCM Type Source #

reconstructParametersInType' :: Action TCM -> Type -> TCM Type Source #

reconstructParametersInTel :: Telescope -> TCM Telescope Source #

reconstructParametersInEqView :: EqualityView -> TCM EqualityView Source #

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

reconstructParameters' :: Action TCM -> Type -> Term -> TCM Term Source #

dropParameters :: TermLike a => a -> TCM a Source #