Agda.TypeChecking.Rules.Application

Documentation

checkArguments :: Comparison -> ExpandHidden -> Range -> [NamedArg Expr] -> Type -> Type -> (ArgsCheckState CheckedTarget -> TCM Term) -> TCM Term

checkArguments cmp 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_

Arguments

:: Comparison

Comparison for target

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

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)

Precondition: Application hd args = appView e.

checkProjAppToKnownPrincipalArg :: Comparison -> Expr -> ProjOrigin -> List1 QName -> Args -> Type -> Int -> Term -> Type -> PrincipalArgTypeMetas -> TCM Term

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

univChecks :: Univ -> TCM ()

suffixToLevel :: Suffix -> Integer