Stefan pushed to branch report/itd at Stefan / Typer
Commits: 143748a4 by Stefan Monnier at 2018-10-05T15:29:53Z -
- - - - -
1 changed file:
- paper.tex
Changes:
===================================== paper.tex ===================================== @@ -614,7 +614,8 @@ which is sound and complete.
\newcommand \Tind[3] {\kw{Ind}(#1:#2)\langle#3\rangle} \newcommand \Tcon[2] {\kw{Con}(#1,#2)} -\newcommand \TIcase[4] {{<}#1{>}\kw{Case}~#2:#3~\kw{of}~\langle#4\rangle} +\newcommand \TIcase[4] {{<}#1{>}\kw{Case}~#2%% :#3 + ~\kw{of}~\langle#4\rangle} \newcommand \Tfix[3] {\kw{Fix}_{#1}~#2:#3~=~}
\newcommand \JIcon[2][x] {#1 \vdash #2;;\kw{con}} @@ -642,12 +643,13 @@ which is sound and complete. \Infer{\JIcon e \ \JIpos \tau}{\JIcon {\Tsarw \tau e}}
%% Actual typing rules - %% FIXME: This lets all inductive types live in Type0!! - \Infer{\Jtyper{\tau}{\Type{\ell}} \ + \Infer{\Jtyper{\tau}{\Type{\ell+1}} \ + \tau = \Tmarw{_}{_}{\Type{\ell}} \ \forall i \ - \Jtyper[\Gamma,x:\tau]{c_i}{\Type{\ell_i}} \ - \JIcon {c_i} \ - \ell_i < \ell} + \Jtyper[\Gamma,x:\tau]{c_i}{\Type{\ell}} \ + \JIcon {c_i} %% \ + %% \ell_i < \ell + } {\Jtyper{\Tind{x}{\tau}{\vec c}}{\tau}}
%% FIXME: This presentation doesn't allow `Con(0,Nat)` but requires @@ -703,20 +705,31 @@ which is sound and complete. \Jdecreasing \nu {\vec b}} {\Jdecreasing \nu {\TIcase{\tau_r}{e}{\tau_e}{\vec b}}}
+ %% The rule for the impredicative case! \Infer{\Jdecreasing \nu e \ \Jdecreasing \nu {\tau_r} \ \Jdecreasing \nu {\tau_e} \\ e = \Tapp{x_e}{\vec _} \ x_e \in \nu \cup { x_i } \ - \tau_e = {\tau_I~{\vec _}} \ - \tau_I = \Tind{x_I}{_}{\vec c} \ - \Jdecreasing \nu {\vec b} \\ \forall i \ b_i = \Tmlam{y}{_}{e_i} \ - c_i = \Tmarw{_}{\tau_i}{_} \ - \nu' = {~ y_j ~|~ \tau_{ij} = \Tapp{x_I}{\vec _} ~} \ - \Jdecreasing {\nu \cup \nu'} {b_i}} + \Jdecreasing {\nu \cup \vec y} {b_i}} {\Jdecreasing \nu {\TIcase{\tau_r}{e}{\tau_e}{\vec b}}} + + %% The rule for the impredicative case! + %% \Infer{\Jdecreasing \nu e \ + %% \Jdecreasing \nu {\tau_r} \ + %% \Jdecreasing \nu {\tau_e} \\ + %% e = \Tapp{x_e}{\vec _} \ + %% x_e \in \nu \cup { x_i } \ + %% \tau_e = {\tau_I~{\vec _}} \ + %% \tau_I = \Tind{x_I}{_}{\vec c} \ + %% \forall i \ + %% b_i = \Tmlam{y}{_}{e_i} \ + %% c_i = \Tmarw{_}{\tau_i}{_} \ + %% \nu' = {~ y_j ~|~ \tau_{ij} = \Tapp{x_I}{\vec _} ~} \ + %% \Jdecreasing {\nu \cup \nu'} {b_i}} + %% {\Jdecreasing \nu {\TIcase{\tau_r}{e}{\tau_e}{\vec b}}} \end{mathpar}
%% Reduction rules
View it on GitLab: https://gitlab.com/monnier/typer/commit/143748a438cd31ae76a5079816937025fef7...
Afficher les réponses par date