ModuleAgda-2.8.0.2Haskell2010

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.

Synopsis

value reconstructParametersInType
value reconstructParametersInType'
value reconstructParametersInTel
value reconstructParametersInEqView
value reconstructParameters
value reconstructParameters'
value reconstructAction
value reconstructAction'
value reconstruct
value extractParameters
value dropParameters

PackageAgda-2.8.0.2
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