Safe Haskell	None
Language	Haskell98

Agda.TypeChecking.ProjectionLike

Synopsis

Documentation

data ProjectionView Source

View for a Def f (Apply a : es) where isProjection f. Used for projection-like fs.

Constructors

ProjectionView	A projection or projection-like function, applied to its principal argument
Fields projViewProj :: QName projViewSelf :: Arg Term projViewSpine :: Elims
LoneProjectionLike QName ArgInfo	Just a lone projection-like function, missing its principal argument (from which we could infer the parameters).
NoProjection Term	Not a projection or projection-like thing.

unProjView :: ProjectionView -> Term Source

Semantics of ProjectionView.

projView :: Term -> TCM ProjectionView Source

Top-level ProjectionView (no reduction).

reduceProjectionLike :: Term -> TCM Term Source

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 :: Bool -> Term -> TCM Term Source

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.

If the Bool is True, a lone projection like function will be turned into a lambda-abstraction, expecting the principal argument. If the Bool is False, it will be returned unaltered.

No precondition. Preserves constructorForm, since it really does only something on (applications of) projection-like functions.

eligibleForProjectionLike :: QName -> TCM Bool Source

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.