Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Rules.Application

Synopsis

- checkArguments :: ExpandHidden -> Range -> [NamedArg Expr] -> Type -> Type -> (MaybeRanges -> Elims -> Type -> CheckedTarget -> TCM Term) -> TCM Term
- checkArguments_ :: ExpandHidden -> Range -> [NamedArg Expr] -> Telescope -> TCM (Elims, Telescope)
- checkApplication :: Comparison -> Expr -> Args -> Expr -> Type -> TCM Term
- inferApplication :: ExpandHidden -> Expr -> Args -> Expr -> TCM (Term, Type)
- checkProjAppToKnownPrincipalArg :: Comparison -> Expr -> ProjOrigin -> NonemptyList QName -> Args -> Type -> Int -> Term -> Type -> TCM Term

# Documentation

checkArguments :: ExpandHidden -> Range -> [NamedArg Expr] -> Type -> Type -> (MaybeRanges -> Elims -> Type -> CheckedTarget -> TCM Term) -> TCM Term Source #

`checkArguments exph r args t0 t k` tries `checkArgumentsE exph args t0 t`. If it succeeds, it continues `k` with the returned results. If it fails, it registers a postponed typechecking problem and returns the resulting new meta variable.

Checks `e := ((_ : t0) args) : t`.

checkArguments_ Source #

Arguments

:: ExpandHidden | Eagerly insert trailing hidden arguments?
-> Range | Range of application.
-> [NamedArg Expr] | Arguments to check.
-> Telescope | Telescope to check arguments against.
-> TCM (Elims, Telescope) | Checked arguments and remaining telescope if successful.

Check that a list of arguments fits a telescope. Inserts hidden arguments as necessary. Returns the type-checked arguments and the remaining telescope.

checkApplication :: Comparison -> Expr -> Args -> Expr -> Type -> TCM Term Source #

`checkApplication hd args e t` checks an application. Precondition: `Application hs args = appView e`

`checkApplication` disambiguates constructors (and continues to `checkConstructorApplication`) and resolves pattern synonyms.

inferApplication :: ExpandHidden -> Expr -> Args -> Expr -> TCM (Term, Type) Source #

Precondition: `Application hd args = appView e`.

checkProjAppToKnownPrincipalArg :: Comparison -> Expr -> ProjOrigin -> NonemptyList QName -> Args -> Type -> Int -> Term -> Type -> TCM Term Source #

Checking the type of an overloaded projection application. See `inferOrCheckProjAppToKnownPrincipalArg`.