ModuleAgda-2.7.0.1Haskell2010

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.

11 values

PackageAgda-2.7.0.1
Exports11
LanguageHaskell2010
LicenceMIT
SourceReconstructParameters.hs

valuereconstructParametersInType :: Type -> TCM Type

valuereconstructParametersInType' :: Action TCM -> Type -> TCM Type

valuereconstructParametersInTel :: Telescope -> TCM Telescope

valuereconstructParametersInEqView :: EqualityView -> TCM EqualityView

valuereconstructParameters :: Type -> Term -> TCM Term

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

valuereconstructAction :: Action TCM

valuereconstructAction' :: Action TCM -> Action TCM

valuereconstruct :: Type -> Term -> TCM Term

valueextractParameters :: QName -> Type -> TCM Args

valuedropParameters :: TermLike a => a -> TCM a