| Safe Haskell | None |
|---|
Agda.TypeChecking.ProjectionLike
- data ProjectionView = ProjectionView {}
- unProjView :: ProjectionView -> Term
- projView :: Term -> TCM (Maybe ProjectionView)
- reduceProjectionLike :: Term -> TCM Term
- elimView :: Term -> TCM Term
- eligibleForProjectionLike :: QName -> TCM Bool
- makeProjection :: QName -> TCM ()
Documentation
data ProjectionView Source
View for a Def f (Apply a : es) where isProjection f.
Used for projection-like fs.
Constructors
| ProjectionView | |
Fields
| |
unProjView :: ProjectionView -> TermSource
Semantics of ProjectionView.
projView :: Term -> TCM (Maybe ProjectionView)Source
Top-level ProjectionView (no reduction).
reduceProjectionLike :: Term -> TCM TermSource
Reduce away top-level projection like functions. (Also reduces projections, but they should not be there, since Internal is in lambda- and projection-beta-normal form.)
elimView :: Term -> TCM TermSource
Turn prefix projection-like function application into postfix ones.
This does just one layer, such that the top spine contains
the projection-like functions as projections.
Used in compareElims in TypeChecking.Conversion
and in CheckInternal.
No precondition. Preserves constructorForm, since it really does only something applications of projection-like functions.
eligibleForProjectionLike :: QName -> TCM BoolSource
Which Deftypes are eligible for the principle argument
of a projection-like function?
makeProjection :: QName -> TCM ()Source
Turn a definition into a projection if it looks like a projection.