| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Rules.Application
Synopsis
- checkArguments :: Comparison -> ExpandHidden -> Range -> [NamedArg Expr] -> Type -> Type -> (ArgsCheckState CheckedTarget -> TCM Term) -> TCM Term
- checkArguments_ :: Comparison -> 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 -> List1 QName -> Args -> Type -> Int -> Term -> Type -> PrincipalArgTypeMetas -> TCM Term
- univChecks :: Univ -> TCM ()
- suffixToLevel :: Suffix -> Integer
Documentation
checkArguments :: Comparison -> ExpandHidden -> Range -> [NamedArg Expr] -> Type -> Type -> (ArgsCheckState CheckedTarget -> TCM Term) -> TCM Term Source #
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.
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 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 -> List1 QName -> Args -> Type -> Int -> Term -> Type -> PrincipalArgTypeMetas -> TCM Term Source #
Checking the type of an overloaded projection application.
See inferOrCheckProjAppToKnownPrincipalArg.
univChecks :: Univ -> TCM () Source #
suffixToLevel :: Suffix -> Integer Source #