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

Safe HaskellNone



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.



checkType :: Type -> TCM () Source #

Entry point for e.g. checking WithFunctionType.

checkType' :: Type -> TCM Sort Source #

Check a type and infer its sort.

Necessary because of PTS rule (SizeUniv, Set i, Set i) but SizeUniv is not included in any Set i.

This algorithm follows Abel, Coquand, Dybjer, MPC 08, Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory

checkSort :: Action -> Sort -> TCM Sort Source #

Check if sort is well-formed.

checkInternal :: Term -> Type -> TCM () Source #

Entry point for term checking.

data Action Source #

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




defaultAction :: Action Source #

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

infer :: Term -> TCM Type Source #

Infer type of a neutral term.

inferSort :: Term -> TCM Sort Source #

Compute the sort of a type.

shouldBeSort :: Type -> TCM Sort Source #

Result is in reduced form.