add a derivation rule for CATCH expression to the specification document

dwango · May 30, 2019 · 077429f · 077429f
1 parent d199721
commit 077429f
Showing 1 changed file with 11 additions and 0 deletions.
diff --git a/docs/derivation-rules.saty b/docs/derivation-rules.saty
@@ -218,6 +218,17 @@ but extended by remote call, local call, list, etc.
         }
       );
     >
+    +small-block<
+      +math(
+        ${
+          \derive?:{\paren{\mathsc{CATCH}}}{
+            | \judgement{A}{e}{\tau}{C} |
+          }{
+            \judgement{A}{\mathtt!{catch}\(e\)}{\mathtt!{any\(\)}}{C}
+          }
+        }
+      );
+    >
     +section{Differences from the original paper}<
       +p{
         The differences from the derivation rules on the original paper are as follows.