Commit 81d24f66 by Mickael Laurent

small fixes

parent f14b6444
 ... ... @@ -326,9 +326,14 @@ rules, because one branch is already unreachable and retyping only occurs with s {\Gamma\bvdash x t \{\{x:t\}\}} { } \qquad \Infer[Const-] { } {\Gamma\bvdash c t \{\}} { \basic{c} \land t = \varnothing } \qquad \Infer[Const] { } {\Gamma\bvdash c t \{\{\}\}} {\Gamma\fvdash c t \{\{\}\}} { } \\ \Infer[Pair] ... ... @@ -437,6 +442,11 @@ $x$ is supposed to be included into $t_x$ or $\neg t_x$. \Infer[Const] { } {\Gamma\fvdash c t \{\{\}\}} { \basic{c} \leq t } \qquad \Infer[Const-] { } {\Gamma\fvdash c t \{\}} { } \\ \Infer[Pair] ... ... @@ -483,11 +493,11 @@ $x$ is supposed to be included into $t_x$ or $\neg t_x$. \{\Leaf(t_i,\Gamma_i)\}_{i\in I} = \tleaves(\tree)} {\Gamma\fvdash {\lambda x:s.\ e}{t} \{\Gamma_i\,\alt\,i\in I\text{ s.t. }t_i\leq t\}} { } \qquad \Infer[Abs-] { } {\Gamma\fvdash {\lambda x:s.\ e}{t} \{\}} { } % \qquad % \Infer[Abs-] % { } % {\Gamma\fvdash {\lambda x:s.\ e}{t} \{\}} % { } \\ \Infer[Let] { ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!