[Git][monnier/typer][report/hmdup] -
Stefan pushed to branch report/hmdup at Stefan / Typer Commits: 45bf474a by Stefan Monnier at 2020-07-01T13:09:15-04:00 - - - - - - 1 changed file: - paper.tex Changes: ===================================== paper.tex ===================================== @@ -730,13 +730,13 @@ incompatible with things like value polymorphism. \begin{figure} \begin{mathpar} - \Infer{ + \Infer[(EF-Var)]{ \Gamma(x) = \tau }{ \JEsynth{x}{\tau}{x} } - \Infer{ + \Infer[(EF-Let)]{ \JEsynth{e_1}{\tau_1}{E_1} \\ \overrightarrow{t\:*} = \kw{fmv}(\Gamma,\tau_1) \\ \JEpoly[\Gamma,x\:\MDArw{t\:*}{\tau_1}]{e_2}{\tau}{E_2} @@ -745,7 +745,7 @@ incompatible with things like value polymorphism. \Let {x} {\TLam{\overrightarrow{t\:*}}{E_1}}{E_2}} } - \Infer{ + \Infer[(EF-App)]{ %% \Jsynth{e_1}{\Arw{\tau_1}{\tau_2}} \\ \Jfresh{u_1,u_2} \\ \JEcheckCoerce{e_1}{\Arw{u_1}{u_2}}{E_1} \\ @@ -754,7 +754,7 @@ incompatible with things like value polymorphism. \JEsynth{e_1~e_2}{u_2}{E_1~E_2} } - \Infer{ + \Infer[(EF-Lam)]{ \Jfresh {\Meta{u_1},\Meta{u_2}} \\ \Junify {\tau}{\Arw{\Meta{u_1}}{\Meta{u_2}}} \\ \JEcheckCoerce[\Gamma,x\:\Meta{u_1}]{e}{\Meta{u_2}}{E} @@ -762,26 +762,26 @@ incompatible with things like value polymorphism. \JEcheck{\Lam x e}{\tau}{\Lam{x\:\Meta{u_1}}{E}} } - \Infer{ + \Infer[(EF-HT)]{ \JEcheckCoerce e \tau E }{ \JEsynth{\HasType{e}{\tau}}{\tau}{E} } - \Infer{ + \Infer[(EF-Infer)]{ \Jfresh{\Meta{u}} \\ \JEcheck{e}{\Meta{u}}{E} }{ %% FIXME: Make it \JsynthCoerce? \JEsynth{e}{\Meta{u}}{E} } - \Infer{ + \Infer[(EF-Poly)]{ \JEcheck[\Gamma,\overrightarrow{t\:*}] e {\tau}{E} }{ \JEcheckCoerce{e}{\MDArw{t\:*}{\tau}}{\TLam{\overrightarrow{t\:*}}{E}} } - \Infer{ + \Infer[(EF-Coerce)]{ %% \Jmono{\tau} \\ \JEsynth{e}{\tau}{E} \\ \JEcoerce {E}{\tau}{E'}{\tau'} @@ -791,7 +791,7 @@ incompatible with things like value polymorphism. %% FIXME: The rules below don't make much sense yet, I think! %% - \Infer{ + \Infer[(CO-Inst)]{ \Jfresh {\vec {\Meta{u}}} \\ \Junify{\tau[\vec {\Meta{u}}/\vec t]}{\tau'} }{ @@ -799,7 +799,7 @@ incompatible with things like value polymorphism. {\TApp{E}{\vec {\Meta{u}}}} {\tau'} } - \Infer{ + \Infer[(CO-Gen)]{ \Jfresh {\vec {\Meta{u}}} \\ \JEcoerce {E} {\tau} {E'} {\tau'[\vec {\Meta{u}}/\vec t]} \\ %% FIXME: Maybe "u" was instantiated to some other View it on GitLab: https://gitlab.com/monnier/typer/-/commit/45bf474a5ceb1f7f7f5f84c7f62885811a... -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/45bf474a5ceb1f7f7f5f84c7f62885811a... You're receiving this email because of your account on gitlab.com.
Afficher les réponses par date
participants (1)
-
Stefan