formalism: Add missing marked zexp well-formedness rules

hazelgrove · Oct 10, 2023 · d2b9018 · d2b9018
1 parent 51d99b7
commit d2b9018
Showing 1 changed file with 75 additions and 0 deletions.
diff --git a/formalism/typed.tex b/formalism/typed.tex
@@ -213,6 +213,81 @@ \subsubsection{Well-formedness}
   }{
     \zWellFormed{\ZCInconType{\ZCMV}}
   }
+
+  \inferrule[WFLam3]{ }{
+    \zWellFormed{\ZLamInconAscT{x}{\ZTMV}{\ECMV}}
+  }
+
+  \inferrule[WFLam4]{
+    \zWellFormed{\ZMV}
+  }{
+    \zWellFormed{\ZLamInconAscE{x}{\TMV}{\ZMV}}
+  }
+
+  \inferrule[WFLam5]{
+  }{
+    \zWellFormed{\ZLamAnaNonMatchedArrowT{x}{\ZTMV}{\ECMV}}
+  }
+
+  \inferrule[WFLam6]{
+    \zWellFormed{\ZMV}
+  }{
+    \zWellFormed{\ZLamAnaNonMatchedArrowE{x}{\TMV}{\ZMV}}
+  }
+
+  \inferrule[WFAp3]{
+    \zWellFormed{\ZMV}
+  }{
+    \zWellFormed{\ZApSynNonMatchedArrowL{\ZMV}{\ECMV}}
+  }
+
+  \inferrule[WFAp4]{
+    \zWellFormed{\ZMV}
+  }{
+    \zWellFormed{\ZApSynNonMatchedArrowR{\ECMV}{\ZMV}}
+  }
+
+  \inferrule[WFInconsistentBranches1]{
+    \zWellFormed{\ZMV}
+  }{
+    \zWellFormed{\ZInconBrC{\ZMV}{\ECMV_1}{\ECMV_2}}
+  }
+
+  \inferrule[WFInconsistentBranches2]{
+    \zWellFormed{\ZMV}
+  }{
+    \zWellFormed{\ZInconBrL{\ECMV_1}{\ZMV}{\ECMV_2}}
+  }
+
+  \inferrule[WFInconsistentBranches3]{
+    \zWellFormed{\ZMV}
+  }{
+    \zWellFormed{\ZInconBrR{\ECMV_1}{\ECMV_2}{\ZMV}}
+  }
+
+  \inferrule[WFPair3]{
+    \zWellFormed{\ZMV}
+  }{
+    \zWellFormed{\ZPairAnaNonMatchedProdL{\ZMV}{\ECMV}}
+  }
+
+  \inferrule[WFPair4]{
+    \zWellFormed{\ZMV}
+  }{
+    \zWellFormed{\ZPairAnaNonMatchedProdR{\ECMV}{\ZMV}}
+  }
+
+  \inferrule[WFProjL2]{
+    \zWellFormed{\ZMV}
+  }{
+    \zWellFormed{\ZProjLSynNonMatchedProd{\ZMV}}
+  }
+
+  \inferrule[WFProjR2]{
+    \zWellFormed{\ZMV}
+  }{
+    \zWellFormed{\ZProjRSynNonMatchedProd{\ZMV}}
+  }
 \end{mathpar}
 
 \subsection{Cursor erasure}