[−][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 |
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. |
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 |
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 |
Type Definitions
LiftState | Internal state when lifting prefix-parameters. |