Commit 2e63fee9 by Mickael Laurent

### abs rule and some todos

parent 573caa66
 ... ... @@ -242,11 +242,6 @@ NOTE: No need to add the case statement to the context in the premises of the \R rules, because one branch is already unreachable and retyping only occurs with stronger environments. \begin{mathpar} % \Infer[Abs] % {\Gamma,(x:s)\vdash e:t} % {\Gamma\vdash\lambda x:s.e: t} % { } % \\ \Infer[LetFirst] { \Gamma\avdash\Gammap\ct a:\{(t_i,\Gamma_i)\}_{i\in I}\\ ... ... @@ -276,9 +271,31 @@ rules, because one branch is already unreachable and retyping only occurs with s { x\in\dom\Gamma \text{ and } x\in\dom\Gammap \text{ and } \Gamma(x) \not\leq \Gammap(x) } \end{mathpar} \begin{mathpar} \Infer[Abs] {\Gamma,(x:s)\avdash{\Gammap}{\ct[\letexp{x}{*}{[]}]} e:\{(t_i,\Gamma_i)\}_{i\in I}\\ \forall i\in I.\ J_i=\{j\,\alt\,j\in I\text{ s.t. } \forall y\in\fv(e).\ \Gamma_j(y)\leq\Gamma_i(y)\}\\ \forall i\in I.\ u_i = \bigwedge_{j\in J_i}(\arrow{\Gamma_j(x)}{( t_i\vee\bigvee_{\substack{j\in J_i\text{ s.t. } \Gamma_i(x)\land\Gamma_j(x)\neq\varnothing\\\text{ and } \exists y\in\bv(e).\ \Gamma_j(y)\not\leq\Gamma_i(y)} } t_j )}) } {\Gamma\vdash\lambda x:s.e: \{(u_i,\Gamma_i)\,\alt\,i\in I\}} { } \end{mathpar} TODO: Check let rule TODO: Abs rules TODO: Check abs rule TODO: What if the initial environment already contains some entries? Or if a variable is used before being declared? Should we add guardians to split rules? ($x\in\bv(\ct)$) TODO: Add * to grammar and add corresponding rules \subsection{Backward typing rules} ... ...
 ... ... @@ -151,6 +151,8 @@ \newcommand{\Odd} {\textsf{Odd}} \newcommand{\subst}[2]{\{#1 \mapsto #2\}} \newcommand{\fv}{\textsf{fv}} \newcommand{\bv}{\textsf{bv}} \newcommand{\var}{\textsf{var}} \newcommand{\Refinef}{\textsf{\textup{Refine}}} \newcommand{\Refine}[2]{\ensuremath{\Refinef_{#1}(#2)}} ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!