Agda.TypeChecking.ReconstructParameters

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

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

reconstructParametersInTel :: Telescope -> TCM Telescope

reconstructParametersInEqView :: EqualityView -> TCM EqualityView

reconstructParameters :: Type -> Term -> TCM Term

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

reconstructAction :: Action TCM

reconstructAction' :: Action TCM -> Action TCM

reconstruct :: Type -> Term -> TCM Term

extractParameters :: QName -> Type -> TCM Args

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