[−][src]Module minitt::check::decl

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

Depends on modules syntax, expr and tcm.

Functions

check_declaration	Originally `checkD` in Mini-TT, but now it's not because this implementation supports prefixed parameters :) Check if a declaration is well-typed and update the context.
check_lift_parameters	Lift all these `parameters` into the context. Returning `TCS` to reuse the variable.
check_recursive_declaration	Extracted from `checkD` in Mini-TT. This part deals with recursive declarations, but without prefixed parameters.
check_simple_declaration	Extracted from `checkD` in Mini-TT. This part deals with non-recursive declarations, but without prefixed parameters.