Safe Haskell | None |
---|---|
Language | Haskell2010 |
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
- checkType :: Type -> TCM ()
- checkType' :: Type -> TCM Sort
- checkSort :: Action -> Sort -> TCM Sort
- checkInternal :: Term -> Type -> TCM ()
- checkInternal' :: Action -> Term -> Type -> TCM Term
- data Action = Action {}
- defaultAction :: Action
- eraseUnusedAction :: Action
- infer :: Term -> TCM Type
- inferSort :: Term -> TCM Sort
- shouldBeSort :: Type -> TCM Sort
Documentation
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
checkInternal
traverses the whole Term
, and we can use this
traversal to modify the term.
Action | |
|
defaultAction :: Action Source #
The default action is to not change the Term
at all.