[][src]Module minitt::check

Type checking: everything related to type-checking.

This module includes:

  • Normal form and read-back functions
  • The four type checking functions -- checkI, checkD, check and checkT.
  • (extended) (sub)typing rules

Depends on module syntax.

Modules

decl

Declaration checker: for prefix parameters, simple declarations and recursive declarations.

expr

Expression checker: infer, instance-of check, normal-form comparison, subtyping, etc.

read_back

Read back: read back functions and normal form definitions.

subtype

Subtyping check: fallback rules of "instance of" checks: infer the expression's type and check if it's the subtype of the expected type.

tcm

Type-Checking Monad: context, state and error.

Functions

check_contextual

For REPL: check an expression under an existing context

check_declaration_main

Similar to checkMain in Mini-TT, but for a declaration.

check_infer_contextual

For REPL: infer the type of an expression under an existing context

check_main

checkMain in Mini-TT.