Agda-2.6.3.20230805: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.CheckInternal

Description

A bidirectional type checker for internal syntax.

Performs checking on unreduced terms. With the exception that projection-like function applications have to be reduced since they break bidirectionality.

Synopsis

Documentation

checkType :: MonadCheckInternal m => Type -> m () Source #

Entry point for e.g. checking WithFunctionType.

infer :: MonadCheckInternal m => Term -> m Type Source #

Infer type of a neutral term.

inferSpine :: MonadCheckInternal m => Action m -> Type -> (Elims -> Term) -> Elims -> m (Type, Elims) Source #

inferSpine action t hd es checks that spine es eliminates value hd [] of type t and returns the remaining type (target of elimination) and the transformed eliminations.

class CheckInternal a where Source #

Minimal complete definition

checkInternal'

Instances

Instances details
CheckInternal Elims Source # 
Instance details

Defined in Agda.TypeChecking.CheckInternal

CheckInternal Level Source # 
Instance details

Defined in Agda.TypeChecking.CheckInternal

CheckInternal PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.CheckInternal

CheckInternal Sort Source # 
Instance details

Defined in Agda.TypeChecking.CheckInternal

CheckInternal Term Source # 
Instance details

Defined in Agda.TypeChecking.CheckInternal

CheckInternal Type Source # 
Instance details

Defined in Agda.TypeChecking.CheckInternal

data Action m Source #

checkInternal traverses the whole Term, and we can use this traversal to modify the term.

Constructors

Action 

Fields

defaultAction :: PureTCM m => Action m Source #

The default action is to not change the Term at all.