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

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

Depends on modules syntax, expr and tcm. $$ \textnormal{checkD}\quad \rho,\Gamma\vdash_l D\Rightarrow \Gamma' $$

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	$$ \frac{\rho \ \texttt{empty} \quad T:\textsf{U} \quad a:T} {\textnormal{checkLiftD}(a,T,\rho)} $$ $$ \frac{\rho\equiv[(v,T)::\rho'] \quad T:\textsf{U} \quad v:T\vdash R:\textsf{U} \quad \Gamma,v:T\vdash\textnormal{checkLiftD}(a,R,\rho')} {\Gamma\vdash\textnormal{checkLiftD}(\lambda v.a,\Pi (v:T).R,\rho)} $$ This is an extension, it's not present in Mini-TT. Lift all these `parameters` into the context. Returning `TCS` to reuse the variable.
check_recursive_declaration	$$ \frac{\rho,\Gamma\vdash_l A \quad \Gamma\vdash p:t=[\textsf{x}_l]\Rightarrow \Gamma_1 \quad (\rho,p=[\textsf{x}_l]),\Gamma\vdash_{l+1} M\Leftarrow t \quad \Gamma\vdash p:t=v\Rightarrow \Gamma_2} {\rho,\Gamma\vdash_l \textsf{rec}\ p:A=M\Rightarrow \Gamma_2} $$ $$ \dbinom{t=⟦A⟧\rho,}{v=⟦M⟧(\rho,\textsf{rec}\ p:A=M)} $$ Extracted from `checkD` in Mini-TT. This part deals with recursive declarations, but without prefixed parameters.
check_simple_declaration	$$ \frac{\rho,\Gamma\vdash_l A \quad \rho,\Gamma\vdash_l M\Leftarrow t \quad \Gamma\vdash p:t=⟦M⟧\rho\Rightarrow \Gamma_1} {\rho,\Gamma\vdash_l p:A=M\Rightarrow \Gamma_1} $$ $$ (t=⟦M⟧\rho) $$ Extracted from `checkD` in Mini-TT. This part deals with non-recursive declarations, but without prefixed parameters.

Internal state when lifting prefix-parameters.