From c3fbf3368f0223b0b0834824f13ab9417a9c6a40 Mon Sep 17 00:00:00 2001
From: William Ball <williampi103@gmail.com>
Date: Sun, 1 Dec 2024 21:38:43 -0800
Subject: [PATCH] accommodated new ascriptions

---
 grammar.js           |    4 +-
 src/grammar.json     |   88 +-
 src/node-types.json  |    8 +
 src/parser.c         | 2038 ++++++++++++++++++++++++------------------
 test/corpus/labs.txt |    8 +-
 5 files changed, 1239 insertions(+), 907 deletions(-)

diff --git a/grammar.js b/grammar.js
index 846e049..6ee2df9 100644
--- a/grammar.js
+++ b/grammar.js
@@ -37,6 +37,7 @@ module.exports = grammar({
     labs : $ => seq(
       choice('λ', 'fun'),
       repeat1($.param_block),
+      optional($.ascription),
       choice('=>', '⇒'),
       $.expr,
     ),
@@ -44,6 +45,7 @@ module.exports = grammar({
     pabs : $ => seq(
       choice('∏', 'forall'),
       repeat1($.param_block),
+      optional($.ascription),
       ',',
       $.expr,
     ),
@@ -75,8 +77,6 @@ module.exports = grammar({
 
     app : $ => repeat1($.term),
 
-    axiom : $ => 'axiom',
-
     arrow : $ => prec.left(1, seq(
       $.app_term,
       choice('->', '→'),
diff --git a/src/grammar.json b/src/grammar.json
index 7e82397..07b841d 100644
--- a/src/grammar.json
+++ b/src/grammar.json
@@ -117,6 +117,18 @@
             "name": "param_block"
           }
         },
+        {
+          "type": "CHOICE",
+          "members": [
+            {
+              "type": "SYMBOL",
+              "name": "ascription"
+            },
+            {
+              "type": "BLANK"
+            }
+          ]
+        },
         {
           "type": "CHOICE",
           "members": [
@@ -159,6 +171,18 @@
             "name": "param_block"
           }
         },
+        {
+          "type": "CHOICE",
+          "members": [
+            {
+              "type": "SYMBOL",
+              "name": "ascription"
+            },
+            {
+              "type": "BLANK"
+            }
+          ]
+        },
         {
           "type": "STRING",
           "value": ","
@@ -282,38 +306,6 @@
         "name": "term"
       }
     },
-    "axiom": {
-      "type": "SEQ",
-      "members": [
-        {
-          "type": "STRING",
-          "value": "axiom"
-        },
-        {
-          "type": "FIELD",
-          "name": "name",
-          "content": {
-            "type": "SYMBOL",
-            "name": "identifier"
-          }
-        },
-        {
-          "type": "REPEAT",
-          "content": {
-            "type": "SYMBOL",
-            "name": "param_block"
-          }
-        },
-        {
-          "type": "SYMBOL",
-          "name": "ascription"
-        },
-        {
-          "type": "STRING",
-          "value": ";"
-        }
-      ]
-    },
     "arrow": {
       "type": "PREC_LEFT",
       "value": 1,
@@ -395,6 +387,38 @@
         }
       ]
     },
+    "axiom": {
+      "type": "SEQ",
+      "members": [
+        {
+          "type": "STRING",
+          "value": "axiom"
+        },
+        {
+          "type": "FIELD",
+          "name": "name",
+          "content": {
+            "type": "SYMBOL",
+            "name": "identifier"
+          }
+        },
+        {
+          "type": "REPEAT",
+          "content": {
+            "type": "SYMBOL",
+            "name": "param_block"
+          }
+        },
+        {
+          "type": "SYMBOL",
+          "name": "ascription"
+        },
+        {
+          "type": "STRING",
+          "value": ";"
+        }
+      ]
+    },
     "definition": {
       "type": "SEQ",
       "members": [
diff --git a/src/node-types.json b/src/node-types.json
index 5f001a2..d1f34c5 100644
--- a/src/node-types.json
+++ b/src/node-types.json
@@ -194,6 +194,10 @@
       "multiple": true,
       "required": true,
       "types": [
+        {
+          "type": "ascription",
+          "named": true
+        },
         {
           "type": "expr",
           "named": true
@@ -232,6 +236,10 @@
       "multiple": true,
       "required": true,
       "types": [
+        {
+          "type": "ascription",
+          "named": true
+        },
         {
           "type": "expr",
           "named": true
diff --git a/src/parser.c b/src/parser.c
index 5074d2d..40e434f 100644
--- a/src/parser.c
+++ b/src/parser.c
@@ -5,7 +5,7 @@
 #endif
 
 #define LANGUAGE_VERSION 14
-#define STATE_COUNT 92
+#define STATE_COUNT 102
 #define LARGE_STATE_COUNT 2
 #define SYMBOL_COUNT 48
 #define ALIAS_COUNT 0
@@ -35,10 +35,10 @@ enum ts_symbol_identifiers {
   anon_sym_let = 17,
   anon_sym_in = 18,
   anon_sym_end = 19,
-  anon_sym_axiom = 20,
-  anon_sym_SEMI = 21,
-  anon_sym_DASH_GT = 22,
-  anon_sym_u2192 = 23,
+  anon_sym_DASH_GT = 20,
+  anon_sym_u2192 = 21,
+  anon_sym_axiom = 22,
+  anon_sym_SEMI = 23,
   anon_sym_def = 24,
   sym_post_command = 25,
   sym_command = 26,
@@ -51,11 +51,11 @@ enum ts_symbol_identifiers {
   sym_binding = 33,
   sym_let = 34,
   sym_app = 35,
-  sym_axiom = 36,
-  sym_arrow = 37,
-  sym_app_term = 38,
-  sym_expr = 39,
-  sym_ascription = 40,
+  sym_arrow = 36,
+  sym_app_term = 37,
+  sym_expr = 38,
+  sym_ascription = 39,
+  sym_axiom = 40,
   sym_definition = 41,
   sym_preprocess = 42,
   aux_sym_program_repeat1 = 43,
@@ -86,10 +86,10 @@ static const char * const ts_symbol_names[] = {
   [anon_sym_let] = "let",
   [anon_sym_in] = "in",
   [anon_sym_end] = "end",
-  [anon_sym_axiom] = "axiom",
-  [anon_sym_SEMI] = ";",
   [anon_sym_DASH_GT] = "->",
   [anon_sym_u2192] = "\u2192",
+  [anon_sym_axiom] = "axiom",
+  [anon_sym_SEMI] = ";",
   [anon_sym_def] = "def",
   [sym_post_command] = "post_command",
   [sym_command] = "command",
@@ -102,11 +102,11 @@ static const char * const ts_symbol_names[] = {
   [sym_binding] = "binding",
   [sym_let] = "let",
   [sym_app] = "app",
-  [sym_axiom] = "axiom",
   [sym_arrow] = "arrow",
   [sym_app_term] = "app_term",
   [sym_expr] = "expr",
   [sym_ascription] = "ascription",
+  [sym_axiom] = "axiom",
   [sym_definition] = "definition",
   [sym_preprocess] = "preprocess",
   [aux_sym_program_repeat1] = "program_repeat1",
@@ -137,10 +137,10 @@ static const TSSymbol ts_symbol_map[] = {
   [anon_sym_let] = anon_sym_let,
   [anon_sym_in] = anon_sym_in,
   [anon_sym_end] = anon_sym_end,
-  [anon_sym_axiom] = anon_sym_axiom,
-  [anon_sym_SEMI] = anon_sym_SEMI,
   [anon_sym_DASH_GT] = anon_sym_DASH_GT,
   [anon_sym_u2192] = anon_sym_u2192,
+  [anon_sym_axiom] = anon_sym_axiom,
+  [anon_sym_SEMI] = anon_sym_SEMI,
   [anon_sym_def] = anon_sym_def,
   [sym_post_command] = sym_post_command,
   [sym_command] = sym_command,
@@ -153,11 +153,11 @@ static const TSSymbol ts_symbol_map[] = {
   [sym_binding] = sym_binding,
   [sym_let] = sym_let,
   [sym_app] = sym_app,
-  [sym_axiom] = sym_axiom,
   [sym_arrow] = sym_arrow,
   [sym_app_term] = sym_app_term,
   [sym_expr] = sym_expr,
   [sym_ascription] = sym_ascription,
+  [sym_axiom] = sym_axiom,
   [sym_definition] = sym_definition,
   [sym_preprocess] = sym_preprocess,
   [aux_sym_program_repeat1] = aux_sym_program_repeat1,
@@ -248,14 +248,6 @@ static const TSSymbolMetadata ts_symbol_metadata[] = {
     .visible = true,
     .named = false,
   },
-  [anon_sym_axiom] = {
-    .visible = true,
-    .named = false,
-  },
-  [anon_sym_SEMI] = {
-    .visible = true,
-    .named = false,
-  },
   [anon_sym_DASH_GT] = {
     .visible = true,
     .named = false,
@@ -264,6 +256,14 @@ static const TSSymbolMetadata ts_symbol_metadata[] = {
     .visible = true,
     .named = false,
   },
+  [anon_sym_axiom] = {
+    .visible = true,
+    .named = false,
+  },
+  [anon_sym_SEMI] = {
+    .visible = true,
+    .named = false,
+  },
   [anon_sym_def] = {
     .visible = true,
     .named = false,
@@ -312,10 +312,6 @@ static const TSSymbolMetadata ts_symbol_metadata[] = {
     .visible = true,
     .named = true,
   },
-  [sym_axiom] = {
-    .visible = true,
-    .named = true,
-  },
   [sym_arrow] = {
     .visible = true,
     .named = true,
@@ -332,6 +328,10 @@ static const TSSymbolMetadata ts_symbol_metadata[] = {
     .visible = true,
     .named = true,
   },
+  [sym_axiom] = {
+    .visible = true,
+    .named = true,
+  },
   [sym_definition] = {
     .visible = true,
     .named = true,
@@ -414,24 +414,24 @@ static const TSStateId ts_primary_state_ids[STATE_COUNT] = {
   [11] = 11,
   [12] = 12,
   [13] = 13,
-  [14] = 6,
+  [14] = 14,
   [15] = 15,
-  [16] = 9,
-  [17] = 15,
-  [18] = 4,
-  [19] = 19,
-  [20] = 20,
-  [21] = 20,
-  [22] = 19,
+  [16] = 7,
+  [17] = 2,
+  [18] = 9,
+  [19] = 11,
+  [20] = 12,
+  [21] = 4,
+  [22] = 22,
   [23] = 23,
   [24] = 24,
   [25] = 25,
   [26] = 26,
   [27] = 27,
-  [28] = 28,
-  [29] = 24,
-  [30] = 23,
-  [31] = 25,
+  [28] = 24,
+  [29] = 23,
+  [30] = 30,
+  [31] = 31,
   [32] = 32,
   [33] = 33,
   [34] = 34,
@@ -440,45 +440,45 @@ static const TSStateId ts_primary_state_ids[STATE_COUNT] = {
   [37] = 37,
   [38] = 38,
   [39] = 39,
-  [40] = 40,
-  [41] = 41,
-  [42] = 42,
+  [40] = 25,
+  [41] = 27,
+  [42] = 26,
   [43] = 43,
   [44] = 44,
   [45] = 45,
-  [46] = 46,
-  [47] = 45,
+  [46] = 45,
+  [47] = 47,
   [48] = 48,
   [49] = 49,
   [50] = 50,
   [51] = 51,
   [52] = 52,
-  [53] = 53,
+  [53] = 51,
   [54] = 54,
   [55] = 55,
   [56] = 56,
-  [57] = 55,
+  [57] = 57,
   [58] = 58,
   [59] = 59,
   [60] = 60,
-  [61] = 43,
+  [61] = 61,
   [62] = 62,
   [63] = 63,
-  [64] = 58,
-  [65] = 63,
+  [64] = 64,
+  [65] = 65,
   [66] = 66,
   [67] = 67,
-  [68] = 68,
+  [68] = 65,
   [69] = 69,
-  [70] = 70,
+  [70] = 44,
   [71] = 71,
-  [72] = 72,
+  [72] = 66,
   [73] = 73,
   [74] = 74,
   [75] = 75,
   [76] = 76,
   [77] = 77,
-  [78] = 78,
+  [78] = 73,
   [79] = 79,
   [80] = 80,
   [81] = 81,
@@ -486,12 +486,22 @@ static const TSStateId ts_primary_state_ids[STATE_COUNT] = {
   [83] = 83,
   [84] = 84,
   [85] = 85,
-  [86] = 76,
+  [86] = 86,
   [87] = 87,
   [88] = 88,
   [89] = 89,
   [90] = 90,
   [91] = 91,
+  [92] = 92,
+  [93] = 93,
+  [94] = 85,
+  [95] = 95,
+  [96] = 96,
+  [97] = 97,
+  [98] = 87,
+  [99] = 99,
+  [100] = 100,
+  [101] = 101,
 };
 
 static bool ts_lex(TSLexer *lexer, TSStateId state) {
@@ -507,7 +517,7 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) {
         ',', 60,
         '-', 6,
         ':', 47,
-        ';', 68,
+        ';', 70,
         '=', 7,
         '@', 18,
         '[', 8,
@@ -518,7 +528,7 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) {
         'i', 24,
         'l', 14,
         0x3bb, 52,
-        0x2192, 70,
+        0x2192, 68,
         0x21d2, 56,
         0x220f, 57,
         0x25a1, 50,
@@ -538,11 +548,14 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) {
         '(', 46,
         ')', 48,
         '*', 49,
+        ',', 60,
         '-', 6,
         ':', 47,
-        ';', 68,
+        ';', 70,
+        '=', 7,
         '[', 8,
-        0x2192, 70,
+        0x2192, 68,
+        0x21d2, 56,
         0x25a1, 50,
       );
       if (('\t' <= lookahead && lookahead <= '\r') ||
@@ -557,7 +570,7 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) {
       if (lookahead == '-') ADVANCE(6);
       if (lookahead == '[') ADVANCE(8);
       if (lookahead == 'e') ADVANCE(40);
-      if (lookahead == 0x2192) ADVANCE(70);
+      if (lookahead == 0x2192) ADVANCE(68);
       if (lookahead == 0x25a1) ADVANCE(50);
       if (('\t' <= lookahead && lookahead <= '\r') ||
           lookahead == ' ') SKIP(3);
@@ -588,7 +601,7 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) {
       END_STATE();
     case 6:
       if (lookahead == '-') ADVANCE(45);
-      if (lookahead == '>') ADVANCE(69);
+      if (lookahead == '>') ADVANCE(67);
       END_STATE();
     case 7:
       if (lookahead == '>') ADVANCE(55);
@@ -636,7 +649,7 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) {
       if (lookahead == 'l') ADVANCE(20);
       END_STATE();
     case 22:
-      if (lookahead == 'm') ADVANCE(67);
+      if (lookahead == 'm') ADVANCE(69);
       END_STATE();
     case 23:
       if (lookahead == 'n') ADVANCE(11);
@@ -846,17 +859,17 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) {
           ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44);
       END_STATE();
     case 67:
-      ACCEPT_TOKEN(anon_sym_axiom);
-      END_STATE();
-    case 68:
-      ACCEPT_TOKEN(anon_sym_SEMI);
-      END_STATE();
-    case 69:
       ACCEPT_TOKEN(anon_sym_DASH_GT);
       END_STATE();
-    case 70:
+    case 68:
       ACCEPT_TOKEN(anon_sym_u2192);
       END_STATE();
+    case 69:
+      ACCEPT_TOKEN(anon_sym_axiom);
+      END_STATE();
+    case 70:
+      ACCEPT_TOKEN(anon_sym_SEMI);
+      END_STATE();
     case 71:
       ACCEPT_TOKEN(anon_sym_def);
       END_STATE();
@@ -908,19 +921,19 @@ static const TSLexMode ts_lex_modes[STATE_COUNT] = {
   [16] = {.lex_state = 4},
   [17] = {.lex_state = 4},
   [18] = {.lex_state = 4},
-  [19] = {.lex_state = 2},
-  [20] = {.lex_state = 2},
-  [21] = {.lex_state = 3},
-  [22] = {.lex_state = 3},
+  [19] = {.lex_state = 4},
+  [20] = {.lex_state = 4},
+  [21] = {.lex_state = 4},
+  [22] = {.lex_state = 4},
   [23] = {.lex_state = 2},
   [24] = {.lex_state = 2},
   [25] = {.lex_state = 2},
-  [26] = {.lex_state = 0},
-  [27] = {.lex_state = 0},
-  [28] = {.lex_state = 0},
+  [26] = {.lex_state = 2},
+  [27] = {.lex_state = 2},
+  [28] = {.lex_state = 3},
   [29] = {.lex_state = 3},
-  [30] = {.lex_state = 3},
-  [31] = {.lex_state = 3},
+  [30] = {.lex_state = 0},
+  [31] = {.lex_state = 0},
   [32] = {.lex_state = 0},
   [33] = {.lex_state = 0},
   [34] = {.lex_state = 0},
@@ -929,9 +942,9 @@ static const TSLexMode ts_lex_modes[STATE_COUNT] = {
   [37] = {.lex_state = 0},
   [38] = {.lex_state = 0},
   [39] = {.lex_state = 0},
-  [40] = {.lex_state = 0},
-  [41] = {.lex_state = 0},
-  [42] = {.lex_state = 0},
+  [40] = {.lex_state = 3},
+  [41] = {.lex_state = 3},
+  [42] = {.lex_state = 3},
   [43] = {.lex_state = 0},
   [44] = {.lex_state = 0},
   [45] = {.lex_state = 0},
@@ -949,9 +962,9 @@ static const TSLexMode ts_lex_modes[STATE_COUNT] = {
   [57] = {.lex_state = 0},
   [58] = {.lex_state = 0},
   [59] = {.lex_state = 0},
-  [60] = {.lex_state = 2},
+  [60] = {.lex_state = 0},
   [61] = {.lex_state = 0},
-  [62] = {.lex_state = 2},
+  [62] = {.lex_state = 0},
   [63] = {.lex_state = 0},
   [64] = {.lex_state = 0},
   [65] = {.lex_state = 0},
@@ -960,27 +973,37 @@ static const TSLexMode ts_lex_modes[STATE_COUNT] = {
   [68] = {.lex_state = 0},
   [69] = {.lex_state = 2},
   [70] = {.lex_state = 0},
-  [71] = {.lex_state = 0},
+  [71] = {.lex_state = 2},
   [72] = {.lex_state = 0},
   [73] = {.lex_state = 0},
-  [74] = {.lex_state = 0},
+  [74] = {.lex_state = 2},
   [75] = {.lex_state = 0},
   [76] = {.lex_state = 0},
   [77] = {.lex_state = 0},
-  [78] = {.lex_state = 2},
+  [78] = {.lex_state = 0},
   [79] = {.lex_state = 0},
   [80] = {.lex_state = 0},
   [81] = {.lex_state = 0},
-  [82] = {.lex_state = 2},
+  [82] = {.lex_state = 0},
   [83] = {.lex_state = 0},
-  [84] = {.lex_state = 1},
-  [85] = {.lex_state = 2},
+  [84] = {.lex_state = 0},
+  [85] = {.lex_state = 0},
   [86] = {.lex_state = 0},
   [87] = {.lex_state = 0},
-  [88] = {.lex_state = 0},
+  [88] = {.lex_state = 2},
   [89] = {.lex_state = 0},
-  [90] = {.lex_state = 0},
+  [90] = {.lex_state = 2},
   [91] = {.lex_state = 0},
+  [92] = {.lex_state = 0},
+  [93] = {.lex_state = 0},
+  [94] = {.lex_state = 0},
+  [95] = {.lex_state = 1},
+  [96] = {.lex_state = 2},
+  [97] = {.lex_state = 0},
+  [98] = {.lex_state = 0},
+  [99] = {.lex_state = 0},
+  [100] = {.lex_state = 0},
+  [101] = {.lex_state = 0},
 };
 
 static const uint16_t ts_parse_table[LARGE_STATE_COUNT][SYMBOL_COUNT] = {
@@ -1004,19 +1027,19 @@ static const uint16_t ts_parse_table[LARGE_STATE_COUNT][SYMBOL_COUNT] = {
     [anon_sym_let] = ACTIONS(1),
     [anon_sym_in] = ACTIONS(1),
     [anon_sym_end] = ACTIONS(1),
-    [anon_sym_axiom] = ACTIONS(1),
-    [anon_sym_SEMI] = ACTIONS(1),
     [anon_sym_DASH_GT] = ACTIONS(1),
     [anon_sym_u2192] = ACTIONS(1),
+    [anon_sym_axiom] = ACTIONS(1),
+    [anon_sym_SEMI] = ACTIONS(1),
     [anon_sym_def] = ACTIONS(1),
     [sym_command] = ACTIONS(1),
   },
   [1] = {
-    [sym_program] = STATE(71),
-    [sym_axiom] = STATE(27),
-    [sym_definition] = STATE(27),
-    [sym_preprocess] = STATE(27),
-    [aux_sym_program_repeat1] = STATE(27),
+    [sym_program] = STATE(83),
+    [sym_axiom] = STATE(38),
+    [sym_definition] = STATE(38),
+    [sym_preprocess] = STATE(38),
+    [aux_sym_program_repeat1] = STATE(38),
     [ts_builtin_sym_end] = ACTIONS(5),
     [sym_comment] = ACTIONS(3),
     [anon_sym_axiom] = ACTIONS(7),
@@ -1045,21 +1068,21 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_forall,
     ACTIONS(29), 1,
       anon_sym_let,
-    STATE(24), 1,
+    STATE(25), 1,
       sym_square,
-    STATE(40), 1,
-      sym_arrow,
-    STATE(43), 1,
-      sym_app_term,
-    STATE(68), 1,
+    STATE(34), 1,
       sym_expr,
+    STATE(37), 1,
+      sym_arrow,
+    STATE(44), 1,
+      sym_app_term,
     ACTIONS(19), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(19), 2,
+    STATE(24), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(32), 4,
+    STATE(36), 4,
       sym_labs,
       sym_pabs,
       sym_let,
@@ -1083,21 +1106,21 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_forall,
     ACTIONS(29), 1,
       anon_sym_let,
-    STATE(24), 1,
+    STATE(25), 1,
       sym_square,
-    STATE(40), 1,
+    STATE(37), 1,
       sym_arrow,
-    STATE(43), 1,
+    STATE(44), 1,
       sym_app_term,
-    STATE(83), 1,
+    STATE(92), 1,
       sym_expr,
     ACTIONS(19), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(19), 2,
+    STATE(24), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(32), 4,
+    STATE(36), 4,
       sym_labs,
       sym_pabs,
       sym_let,
@@ -1121,21 +1144,21 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_forall,
     ACTIONS(29), 1,
       anon_sym_let,
-    STATE(24), 1,
+    STATE(25), 1,
       sym_square,
-    STATE(40), 1,
+    STATE(37), 1,
       sym_arrow,
-    STATE(43), 1,
+    STATE(44), 1,
       sym_app_term,
-    STATE(76), 1,
+    STATE(85), 1,
       sym_expr,
     ACTIONS(19), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(19), 2,
+    STATE(24), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(32), 4,
+    STATE(36), 4,
       sym_labs,
       sym_pabs,
       sym_let,
@@ -1159,21 +1182,21 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_forall,
     ACTIONS(29), 1,
       anon_sym_let,
-    STATE(24), 1,
+    STATE(25), 1,
       sym_square,
-    STATE(40), 1,
+    STATE(37), 1,
       sym_arrow,
-    STATE(43), 1,
+    STATE(44), 1,
       sym_app_term,
-    STATE(91), 1,
+    STATE(99), 1,
       sym_expr,
     ACTIONS(19), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(19), 2,
+    STATE(24), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(32), 4,
+    STATE(36), 4,
       sym_labs,
       sym_pabs,
       sym_let,
@@ -1197,21 +1220,21 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_forall,
     ACTIONS(29), 1,
       anon_sym_let,
-    STATE(24), 1,
+    STATE(25), 1,
       sym_square,
-    STATE(33), 1,
-      sym_expr,
-    STATE(40), 1,
+    STATE(37), 1,
       sym_arrow,
-    STATE(43), 1,
+    STATE(44), 1,
       sym_app_term,
+    STATE(80), 1,
+      sym_expr,
     ACTIONS(19), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(19), 2,
+    STATE(24), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(32), 4,
+    STATE(36), 4,
       sym_labs,
       sym_pabs,
       sym_let,
@@ -1235,21 +1258,21 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_forall,
     ACTIONS(29), 1,
       anon_sym_let,
-    STATE(24), 1,
+    STATE(25), 1,
       sym_square,
-    STATE(40), 1,
-      sym_arrow,
-    STATE(43), 1,
-      sym_app_term,
-    STATE(79), 1,
+    STATE(32), 1,
       sym_expr,
+    STATE(37), 1,
+      sym_arrow,
+    STATE(44), 1,
+      sym_app_term,
     ACTIONS(19), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(19), 2,
+    STATE(24), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(32), 4,
+    STATE(36), 4,
       sym_labs,
       sym_pabs,
       sym_let,
@@ -1273,21 +1296,21 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_forall,
     ACTIONS(29), 1,
       anon_sym_let,
-    STATE(24), 1,
+    STATE(25), 1,
       sym_square,
-    STATE(40), 1,
+    STATE(37), 1,
       sym_arrow,
-    STATE(43), 1,
+    STATE(44), 1,
       sym_app_term,
-    STATE(88), 1,
+    STATE(82), 1,
       sym_expr,
     ACTIONS(19), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(19), 2,
+    STATE(24), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(32), 4,
+    STATE(36), 4,
       sym_labs,
       sym_pabs,
       sym_let,
@@ -1311,21 +1334,21 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_forall,
     ACTIONS(29), 1,
       anon_sym_let,
-    STATE(24), 1,
+    STATE(25), 1,
       sym_square,
-    STATE(36), 1,
+    STATE(33), 1,
       sym_expr,
-    STATE(40), 1,
+    STATE(37), 1,
       sym_arrow,
-    STATE(43), 1,
+    STATE(44), 1,
       sym_app_term,
     ACTIONS(19), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(19), 2,
+    STATE(24), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(32), 4,
+    STATE(36), 4,
       sym_labs,
       sym_pabs,
       sym_let,
@@ -1333,37 +1356,37 @@ static const uint16_t ts_small_parse_table[] = {
   [432] = 16,
     ACTIONS(3), 1,
       sym_comment,
+    ACTIONS(13), 1,
+      sym_identifier,
+    ACTIONS(15), 1,
+      anon_sym_LPAREN,
+    ACTIONS(17), 1,
+      sym_star,
+    ACTIONS(21), 1,
+      anon_sym_u03bb,
+    ACTIONS(23), 1,
+      anon_sym_fun,
+    ACTIONS(25), 1,
+      anon_sym_u220f,
+    ACTIONS(27), 1,
+      anon_sym_forall,
     ACTIONS(29), 1,
       anon_sym_let,
-    ACTIONS(31), 1,
-      sym_identifier,
-    ACTIONS(33), 1,
-      anon_sym_LPAREN,
-    ACTIONS(35), 1,
-      sym_star,
-    ACTIONS(39), 1,
-      anon_sym_u03bb,
-    ACTIONS(41), 1,
-      anon_sym_fun,
-    ACTIONS(43), 1,
-      anon_sym_u220f,
-    ACTIONS(45), 1,
-      anon_sym_forall,
-    STATE(29), 1,
+    STATE(25), 1,
       sym_square,
-    STATE(40), 1,
+    STATE(37), 1,
       sym_arrow,
-    STATE(61), 1,
+    STATE(44), 1,
       sym_app_term,
-    STATE(77), 1,
+    STATE(54), 1,
       sym_expr,
-    ACTIONS(37), 2,
+    ACTIONS(19), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(22), 2,
+    STATE(24), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(32), 4,
+    STATE(36), 4,
       sym_labs,
       sym_pabs,
       sym_let,
@@ -1387,21 +1410,21 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_forall,
     ACTIONS(29), 1,
       anon_sym_let,
-    STATE(24), 1,
+    STATE(25), 1,
       sym_square,
-    STATE(40), 1,
-      sym_arrow,
-    STATE(43), 1,
-      sym_app_term,
-    STATE(81), 1,
+    STATE(30), 1,
       sym_expr,
+    STATE(37), 1,
+      sym_arrow,
+    STATE(44), 1,
+      sym_app_term,
     ACTIONS(19), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(19), 2,
+    STATE(24), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(32), 4,
+    STATE(36), 4,
       sym_labs,
       sym_pabs,
       sym_let,
@@ -1425,21 +1448,21 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_forall,
     ACTIONS(29), 1,
       anon_sym_let,
-    STATE(24), 1,
+    STATE(25), 1,
       sym_square,
-    STATE(40), 1,
-      sym_arrow,
-    STATE(43), 1,
-      sym_app_term,
-    STATE(72), 1,
+    STATE(31), 1,
       sym_expr,
+    STATE(37), 1,
+      sym_arrow,
+    STATE(44), 1,
+      sym_app_term,
     ACTIONS(19), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(19), 2,
+    STATE(24), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(32), 4,
+    STATE(36), 4,
       sym_labs,
       sym_pabs,
       sym_let,
@@ -1463,21 +1486,21 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_forall,
     ACTIONS(29), 1,
       anon_sym_let,
-    STATE(24), 1,
+    STATE(25), 1,
       sym_square,
-    STATE(40), 1,
+    STATE(37), 1,
       sym_arrow,
-    STATE(43), 1,
+    STATE(44), 1,
       sym_app_term,
-    STATE(75), 1,
+    STATE(91), 1,
       sym_expr,
     ACTIONS(19), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(19), 2,
+    STATE(24), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(32), 4,
+    STATE(36), 4,
       sym_labs,
       sym_pabs,
       sym_let,
@@ -1485,37 +1508,37 @@ static const uint16_t ts_small_parse_table[] = {
   [648] = 16,
     ACTIONS(3), 1,
       sym_comment,
+    ACTIONS(13), 1,
+      sym_identifier,
+    ACTIONS(15), 1,
+      anon_sym_LPAREN,
+    ACTIONS(17), 1,
+      sym_star,
+    ACTIONS(21), 1,
+      anon_sym_u03bb,
+    ACTIONS(23), 1,
+      anon_sym_fun,
+    ACTIONS(25), 1,
+      anon_sym_u220f,
+    ACTIONS(27), 1,
+      anon_sym_forall,
     ACTIONS(29), 1,
       anon_sym_let,
-    ACTIONS(31), 1,
-      sym_identifier,
-    ACTIONS(33), 1,
-      anon_sym_LPAREN,
-    ACTIONS(35), 1,
-      sym_star,
-    ACTIONS(39), 1,
-      anon_sym_u03bb,
-    ACTIONS(41), 1,
-      anon_sym_fun,
-    ACTIONS(43), 1,
-      anon_sym_u220f,
-    ACTIONS(45), 1,
-      anon_sym_forall,
-    STATE(29), 1,
+    STATE(25), 1,
       sym_square,
-    STATE(33), 1,
-      sym_expr,
-    STATE(40), 1,
+    STATE(37), 1,
       sym_arrow,
-    STATE(61), 1,
+    STATE(44), 1,
       sym_app_term,
-    ACTIONS(37), 2,
+    STATE(97), 1,
+      sym_expr,
+    ACTIONS(19), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(22), 2,
+    STATE(24), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(32), 4,
+    STATE(36), 4,
       sym_labs,
       sym_pabs,
       sym_let,
@@ -1539,21 +1562,21 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_forall,
     ACTIONS(29), 1,
       anon_sym_let,
-    STATE(24), 1,
+    STATE(25), 1,
       sym_square,
     STATE(37), 1,
-      sym_expr,
-    STATE(40), 1,
       sym_arrow,
-    STATE(43), 1,
+    STATE(44), 1,
       sym_app_term,
+    STATE(81), 1,
+      sym_expr,
     ACTIONS(19), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(19), 2,
+    STATE(24), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(32), 4,
+    STATE(36), 4,
       sym_labs,
       sym_pabs,
       sym_let,
@@ -1577,21 +1600,21 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_u220f,
     ACTIONS(45), 1,
       anon_sym_forall,
-    STATE(29), 1,
-      sym_square,
-    STATE(36), 1,
+    STATE(32), 1,
       sym_expr,
-    STATE(40), 1,
+    STATE(37), 1,
       sym_arrow,
-    STATE(61), 1,
+    STATE(40), 1,
+      sym_square,
+    STATE(70), 1,
       sym_app_term,
     ACTIONS(37), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(22), 2,
+    STATE(28), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(32), 4,
+    STATE(36), 4,
       sym_labs,
       sym_pabs,
       sym_let,
@@ -1615,26 +1638,140 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_u220f,
     ACTIONS(45), 1,
       anon_sym_forall,
-    STATE(29), 1,
-      sym_square,
-    STATE(37), 1,
+    STATE(34), 1,
       sym_expr,
-    STATE(40), 1,
+    STATE(37), 1,
       sym_arrow,
-    STATE(61), 1,
+    STATE(40), 1,
+      sym_square,
+    STATE(70), 1,
       sym_app_term,
     ACTIONS(37), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(22), 2,
+    STATE(28), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(32), 4,
+    STATE(36), 4,
       sym_labs,
       sym_pabs,
       sym_let,
       sym_app,
   [864] = 16,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(29), 1,
+      anon_sym_let,
+    ACTIONS(31), 1,
+      sym_identifier,
+    ACTIONS(33), 1,
+      anon_sym_LPAREN,
+    ACTIONS(35), 1,
+      sym_star,
+    ACTIONS(39), 1,
+      anon_sym_u03bb,
+    ACTIONS(41), 1,
+      anon_sym_fun,
+    ACTIONS(43), 1,
+      anon_sym_u220f,
+    ACTIONS(45), 1,
+      anon_sym_forall,
+    STATE(33), 1,
+      sym_expr,
+    STATE(37), 1,
+      sym_arrow,
+    STATE(40), 1,
+      sym_square,
+    STATE(70), 1,
+      sym_app_term,
+    ACTIONS(37), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(28), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+    STATE(36), 4,
+      sym_labs,
+      sym_pabs,
+      sym_let,
+      sym_app,
+  [918] = 16,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(29), 1,
+      anon_sym_let,
+    ACTIONS(31), 1,
+      sym_identifier,
+    ACTIONS(33), 1,
+      anon_sym_LPAREN,
+    ACTIONS(35), 1,
+      sym_star,
+    ACTIONS(39), 1,
+      anon_sym_u03bb,
+    ACTIONS(41), 1,
+      anon_sym_fun,
+    ACTIONS(43), 1,
+      anon_sym_u220f,
+    ACTIONS(45), 1,
+      anon_sym_forall,
+    STATE(30), 1,
+      sym_expr,
+    STATE(37), 1,
+      sym_arrow,
+    STATE(40), 1,
+      sym_square,
+    STATE(70), 1,
+      sym_app_term,
+    ACTIONS(37), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(28), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+    STATE(36), 4,
+      sym_labs,
+      sym_pabs,
+      sym_let,
+      sym_app,
+  [972] = 16,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(29), 1,
+      anon_sym_let,
+    ACTIONS(31), 1,
+      sym_identifier,
+    ACTIONS(33), 1,
+      anon_sym_LPAREN,
+    ACTIONS(35), 1,
+      sym_star,
+    ACTIONS(39), 1,
+      anon_sym_u03bb,
+    ACTIONS(41), 1,
+      anon_sym_fun,
+    ACTIONS(43), 1,
+      anon_sym_u220f,
+    ACTIONS(45), 1,
+      anon_sym_forall,
+    STATE(31), 1,
+      sym_expr,
+    STATE(37), 1,
+      sym_arrow,
+    STATE(40), 1,
+      sym_square,
+    STATE(70), 1,
+      sym_app_term,
+    ACTIONS(37), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(28), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+    STATE(36), 4,
+      sym_labs,
+      sym_pabs,
+      sym_let,
+      sym_app,
+  [1026] = 16,
     ACTIONS(3), 1,
       sym_comment,
     ACTIONS(13), 1,
@@ -1653,31 +1790,94 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_forall,
     ACTIONS(29), 1,
       anon_sym_let,
-    STATE(24), 1,
+    STATE(25), 1,
       sym_square,
-    STATE(40), 1,
+    STATE(37), 1,
       sym_arrow,
-    STATE(43), 1,
+    STATE(44), 1,
       sym_app_term,
-    STATE(86), 1,
+    STATE(94), 1,
       sym_expr,
     ACTIONS(19), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(19), 2,
+    STATE(24), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(32), 4,
+    STATE(36), 4,
       sym_labs,
       sym_pabs,
       sym_let,
       sym_app,
-  [918] = 7,
+  [1080] = 16,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(29), 1,
+      anon_sym_let,
+    ACTIONS(31), 1,
+      sym_identifier,
+    ACTIONS(33), 1,
+      anon_sym_LPAREN,
+    ACTIONS(35), 1,
+      sym_star,
+    ACTIONS(39), 1,
+      anon_sym_u03bb,
+    ACTIONS(41), 1,
+      anon_sym_fun,
+    ACTIONS(43), 1,
+      anon_sym_u220f,
+    ACTIONS(45), 1,
+      anon_sym_forall,
+    STATE(37), 1,
+      sym_arrow,
+    STATE(40), 1,
+      sym_square,
+    STATE(70), 1,
+      sym_app_term,
+    STATE(84), 1,
+      sym_expr,
+    ACTIONS(37), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(28), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+    STATE(36), 4,
+      sym_labs,
+      sym_pabs,
+      sym_let,
+      sym_app,
+  [1134] = 7,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(50), 1,
+      anon_sym_LPAREN,
+    STATE(25), 1,
+      sym_square,
+    ACTIONS(47), 2,
+      sym_identifier,
+      sym_star,
+    ACTIONS(55), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(23), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+    ACTIONS(53), 8,
+      anon_sym_RPAREN,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+      anon_sym_COMMA,
+      anon_sym_COLON_EQ,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+      anon_sym_SEMI,
+  [1166] = 7,
     ACTIONS(3), 1,
       sym_comment,
     ACTIONS(15), 1,
       anon_sym_LPAREN,
-    STATE(24), 1,
+    STATE(25), 1,
       sym_square,
     ACTIONS(17), 2,
       sym_identifier,
@@ -1685,60 +1885,70 @@ static const uint16_t ts_small_parse_table[] = {
     ACTIONS(19), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(20), 2,
+    STATE(23), 2,
       sym_term,
       aux_sym_app_repeat1,
-    ACTIONS(47), 5,
+    ACTIONS(58), 8,
       anon_sym_RPAREN,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+      anon_sym_COMMA,
       anon_sym_COLON_EQ,
-      anon_sym_SEMI,
       anon_sym_DASH_GT,
       anon_sym_u2192,
-  [947] = 7,
+      anon_sym_SEMI,
+  [1198] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(52), 1,
-      anon_sym_LPAREN,
-    STATE(24), 1,
-      sym_square,
-    ACTIONS(49), 2,
+    ACTIONS(60), 13,
       sym_identifier,
+      anon_sym_LPAREN,
+      anon_sym_RPAREN,
       sym_star,
-    ACTIONS(57), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(20), 2,
-      sym_term,
-      aux_sym_app_repeat1,
-    ACTIONS(55), 5,
-      anon_sym_RPAREN,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+      anon_sym_COMMA,
       anon_sym_COLON_EQ,
-      anon_sym_SEMI,
       anon_sym_DASH_GT,
       anon_sym_u2192,
-  [976] = 9,
+      anon_sym_SEMI,
+  [1217] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(60), 1,
+    ACTIONS(62), 13,
       sym_identifier,
-    ACTIONS(63), 1,
       anon_sym_LPAREN,
-    ACTIONS(66), 1,
+      anon_sym_RPAREN,
       sym_star,
-    ACTIONS(72), 1,
-      anon_sym_end,
-    STATE(29), 1,
-      sym_square,
-    ACTIONS(55), 2,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-    ACTIONS(69), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(21), 2,
-      sym_term,
-      aux_sym_app_repeat1,
-  [1007] = 9,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+      anon_sym_COMMA,
+      anon_sym_COLON_EQ,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+      anon_sym_SEMI,
+  [1236] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(64), 13,
+      sym_identifier,
+      anon_sym_LPAREN,
+      anon_sym_RPAREN,
+      sym_star,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+      anon_sym_COMMA,
+      anon_sym_COLON_EQ,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+      anon_sym_SEMI,
+  [1255] = 9,
     ACTIONS(3), 1,
       sym_comment,
     ACTIONS(31), 1,
@@ -1747,77 +1957,146 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_LPAREN,
     ACTIONS(35), 1,
       sym_star,
-    ACTIONS(74), 1,
+    ACTIONS(66), 1,
       anon_sym_end,
-    STATE(29), 1,
+    STATE(40), 1,
       sym_square,
     ACTIONS(37), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    ACTIONS(47), 2,
+    ACTIONS(58), 2,
       anon_sym_DASH_GT,
       anon_sym_u2192,
-    STATE(21), 2,
+    STATE(29), 2,
       sym_term,
       aux_sym_app_repeat1,
-  [1038] = 2,
+  [1286] = 9,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(76), 10,
+    ACTIONS(68), 1,
       sym_identifier,
+    ACTIONS(71), 1,
       anon_sym_LPAREN,
-      anon_sym_RPAREN,
+    ACTIONS(74), 1,
       sym_star,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-      anon_sym_COLON_EQ,
-      anon_sym_SEMI,
+    ACTIONS(80), 1,
+      anon_sym_end,
+    STATE(40), 1,
+      sym_square,
+    ACTIONS(53), 2,
       anon_sym_DASH_GT,
       anon_sym_u2192,
-  [1054] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(78), 10,
-      sym_identifier,
-      anon_sym_LPAREN,
-      anon_sym_RPAREN,
-      sym_star,
+    ACTIONS(77), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-      anon_sym_COLON_EQ,
-      anon_sym_SEMI,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-  [1070] = 2,
+    STATE(29), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+  [1317] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(80), 10,
-      sym_identifier,
-      anon_sym_LPAREN,
+    ACTIONS(82), 9,
       anon_sym_RPAREN,
-      sym_star,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-      anon_sym_COLON_EQ,
-      anon_sym_SEMI,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-  [1086] = 5,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(82), 1,
-      anon_sym_LPAREN,
-    ACTIONS(85), 1,
-      anon_sym_COLON,
-    STATE(26), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-    ACTIONS(87), 4,
       anon_sym_EQ_GT,
       anon_sym_u21d2,
       anon_sym_COMMA,
       anon_sym_COLON_EQ,
-  [1106] = 6,
+      anon_sym_end,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+      anon_sym_SEMI,
+  [1332] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(84), 9,
+      anon_sym_RPAREN,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+      anon_sym_COMMA,
+      anon_sym_COLON_EQ,
+      anon_sym_end,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+      anon_sym_SEMI,
+  [1347] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(86), 9,
+      anon_sym_RPAREN,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+      anon_sym_COMMA,
+      anon_sym_COLON_EQ,
+      anon_sym_end,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+      anon_sym_SEMI,
+  [1362] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(88), 9,
+      anon_sym_RPAREN,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+      anon_sym_COMMA,
+      anon_sym_COLON_EQ,
+      anon_sym_end,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+      anon_sym_SEMI,
+  [1377] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(90), 9,
+      anon_sym_RPAREN,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+      anon_sym_COMMA,
+      anon_sym_COLON_EQ,
+      anon_sym_end,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+      anon_sym_SEMI,
+  [1392] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(92), 9,
+      anon_sym_RPAREN,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+      anon_sym_COMMA,
+      anon_sym_COLON_EQ,
+      anon_sym_end,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+      anon_sym_SEMI,
+  [1407] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(94), 9,
+      anon_sym_RPAREN,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+      anon_sym_COMMA,
+      anon_sym_COLON_EQ,
+      anon_sym_end,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+      anon_sym_SEMI,
+  [1422] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(96), 9,
+      anon_sym_RPAREN,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+      anon_sym_COMMA,
+      anon_sym_COLON_EQ,
+      anon_sym_end,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+      anon_sym_SEMI,
+  [1437] = 6,
     ACTIONS(3), 1,
       sym_comment,
     ACTIONS(7), 1,
@@ -1826,322 +2105,289 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_def,
     ACTIONS(11), 1,
       sym_command,
-    ACTIONS(89), 1,
+    ACTIONS(98), 1,
       ts_builtin_sym_end,
-    STATE(28), 4,
+    STATE(43), 4,
       sym_axiom,
       sym_definition,
       sym_preprocess,
       aux_sym_program_repeat1,
-  [1128] = 6,
+  [1459] = 5,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(91), 1,
-      ts_builtin_sym_end,
-    ACTIONS(93), 1,
-      anon_sym_axiom,
-    ACTIONS(96), 1,
-      anon_sym_def,
-    ACTIONS(99), 1,
-      sym_command,
-    STATE(28), 4,
-      sym_axiom,
-      sym_definition,
-      sym_preprocess,
-      aux_sym_program_repeat1,
-  [1150] = 3,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(102), 2,
-      sym_identifier,
-      anon_sym_end,
-    ACTIONS(78), 6,
+    ACTIONS(100), 1,
       anon_sym_LPAREN,
-      sym_star,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-  [1166] = 3,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(104), 2,
-      sym_identifier,
-      anon_sym_end,
-    ACTIONS(76), 6,
-      anon_sym_LPAREN,
-      sym_star,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-  [1182] = 3,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(106), 2,
-      sym_identifier,
-      anon_sym_end,
-    ACTIONS(80), 6,
-      anon_sym_LPAREN,
-      sym_star,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-  [1198] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(108), 6,
-      anon_sym_RPAREN,
-      anon_sym_COLON_EQ,
-      anon_sym_end,
-      anon_sym_SEMI,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-  [1210] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(110), 6,
-      anon_sym_RPAREN,
-      anon_sym_COLON_EQ,
-      anon_sym_end,
-      anon_sym_SEMI,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-  [1222] = 6,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(112), 1,
-      anon_sym_LPAREN,
-    ACTIONS(114), 1,
+    ACTIONS(103), 1,
       anon_sym_COLON,
-    ACTIONS(116), 1,
+    STATE(39), 2,
+      sym_param_block,
+      aux_sym_labs_repeat1,
+    ACTIONS(105), 4,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+      anon_sym_COMMA,
       anon_sym_COLON_EQ,
-    STATE(74), 1,
+  [1479] = 3,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(107), 2,
+      sym_identifier,
+      anon_sym_end,
+    ACTIONS(60), 6,
+      anon_sym_LPAREN,
+      sym_star,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+  [1495] = 3,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(109), 2,
+      sym_identifier,
+      anon_sym_end,
+    ACTIONS(64), 6,
+      anon_sym_LPAREN,
+      sym_star,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+  [1511] = 3,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(111), 2,
+      sym_identifier,
+      anon_sym_end,
+    ACTIONS(62), 6,
+      anon_sym_LPAREN,
+      sym_star,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+  [1527] = 6,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(113), 1,
+      ts_builtin_sym_end,
+    ACTIONS(115), 1,
+      anon_sym_axiom,
+    ACTIONS(118), 1,
+      anon_sym_def,
+    ACTIONS(121), 1,
+      sym_command,
+    STATE(43), 4,
+      sym_axiom,
+      sym_definition,
+      sym_preprocess,
+      aux_sym_program_repeat1,
+  [1549] = 3,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(124), 2,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+    ACTIONS(96), 6,
+      anon_sym_RPAREN,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+      anon_sym_COMMA,
+      anon_sym_COLON_EQ,
+      anon_sym_SEMI,
+  [1565] = 6,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(126), 1,
+      anon_sym_LPAREN,
+    ACTIONS(128), 1,
+      anon_sym_COLON,
+    STATE(73), 1,
+      sym_ascription,
+    ACTIONS(130), 2,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+    STATE(39), 2,
+      sym_param_block,
+      aux_sym_labs_repeat1,
+  [1586] = 6,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(126), 1,
+      anon_sym_LPAREN,
+    ACTIONS(128), 1,
+      anon_sym_COLON,
+    STATE(78), 1,
+      sym_ascription,
+    ACTIONS(132), 2,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+    STATE(39), 2,
+      sym_param_block,
+      aux_sym_labs_repeat1,
+  [1607] = 6,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(126), 1,
+      anon_sym_LPAREN,
+    ACTIONS(134), 1,
+      anon_sym_COLON,
+    ACTIONS(136), 1,
+      anon_sym_COLON_EQ,
+    STATE(101), 1,
+      sym_ascription,
+    STATE(50), 2,
+      sym_param_block,
+      aux_sym_labs_repeat1,
+  [1627] = 3,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(140), 1,
+      anon_sym_COLON,
+    ACTIONS(138), 5,
+      anon_sym_LPAREN,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+      anon_sym_COMMA,
+      anon_sym_COLON_EQ,
+  [1641] = 6,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(126), 1,
+      anon_sym_LPAREN,
+    ACTIONS(134), 1,
+      anon_sym_COLON,
+    ACTIONS(142), 1,
+      anon_sym_COLON_EQ,
+    STATE(86), 1,
+      sym_ascription,
+    STATE(52), 2,
+      sym_param_block,
+      aux_sym_labs_repeat1,
+  [1661] = 6,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(126), 1,
+      anon_sym_LPAREN,
+    ACTIONS(134), 1,
+      anon_sym_COLON,
+    ACTIONS(144), 1,
+      anon_sym_COLON_EQ,
+    STATE(93), 1,
       sym_ascription,
     STATE(39), 2,
       sym_param_block,
       aux_sym_labs_repeat1,
-  [1242] = 3,
+  [1681] = 6,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(120), 1,
-      anon_sym_COLON,
-    ACTIONS(118), 5,
-      anon_sym_LPAREN,
-      anon_sym_EQ_GT,
-      anon_sym_u21d2,
-      anon_sym_COMMA,
-      anon_sym_COLON_EQ,
-  [1256] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(122), 6,
-      anon_sym_RPAREN,
-      anon_sym_COLON_EQ,
-      anon_sym_end,
-      anon_sym_SEMI,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-  [1268] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(124), 6,
-      anon_sym_RPAREN,
-      anon_sym_COLON_EQ,
-      anon_sym_end,
-      anon_sym_SEMI,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-  [1280] = 6,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(112), 1,
-      anon_sym_LPAREN,
-    ACTIONS(114), 1,
-      anon_sym_COLON,
     ACTIONS(126), 1,
-      anon_sym_COLON_EQ,
-    STATE(73), 1,
-      sym_ascription,
-    STATE(42), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-  [1300] = 6,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(112), 1,
       anon_sym_LPAREN,
-    ACTIONS(114), 1,
-      anon_sym_COLON,
     ACTIONS(128), 1,
-      anon_sym_COLON_EQ,
+      anon_sym_COLON,
+    ACTIONS(146), 1,
+      anon_sym_COMMA,
     STATE(87), 1,
       sym_ascription,
-    STATE(26), 2,
+    STATE(39), 2,
       sym_param_block,
       aux_sym_labs_repeat1,
-  [1320] = 2,
+  [1701] = 6,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(130), 6,
-      anon_sym_RPAREN,
-      anon_sym_COLON_EQ,
-      anon_sym_end,
-      anon_sym_SEMI,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-  [1332] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(132), 6,
-      anon_sym_RPAREN,
-      anon_sym_COLON_EQ,
-      anon_sym_end,
-      anon_sym_SEMI,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-  [1344] = 6,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(112), 1,
+    ACTIONS(126), 1,
       anon_sym_LPAREN,
-    ACTIONS(114), 1,
-      anon_sym_COLON,
     ACTIONS(134), 1,
+      anon_sym_COLON,
+    ACTIONS(148), 1,
       anon_sym_COLON_EQ,
+    STATE(100), 1,
+      sym_ascription,
+    STATE(39), 2,
+      sym_param_block,
+      aux_sym_labs_repeat1,
+  [1721] = 6,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(126), 1,
+      anon_sym_LPAREN,
+    ACTIONS(128), 1,
+      anon_sym_COLON,
+    ACTIONS(150), 1,
+      anon_sym_COMMA,
+    STATE(98), 1,
+      sym_ascription,
+    STATE(39), 2,
+      sym_param_block,
+      aux_sym_labs_repeat1,
+  [1741] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(152), 5,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+      anon_sym_COMMA,
+      anon_sym_COLON_EQ,
+      anon_sym_SEMI,
+  [1752] = 5,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(126), 1,
+      anon_sym_LPAREN,
+    ACTIONS(128), 1,
+      anon_sym_COLON,
+    STATE(79), 1,
+      sym_ascription,
+    STATE(56), 2,
+      sym_param_block,
+      aux_sym_labs_repeat1,
+  [1769] = 5,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(126), 1,
+      anon_sym_LPAREN,
+    ACTIONS(128), 1,
+      anon_sym_COLON,
     STATE(89), 1,
       sym_ascription,
-    STATE(26), 2,
+    STATE(39), 2,
       sym_param_block,
       aux_sym_labs_repeat1,
-  [1364] = 3,
+  [1786] = 4,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(136), 2,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-    ACTIONS(130), 3,
-      anon_sym_RPAREN,
-      anon_sym_COLON_EQ,
-      anon_sym_SEMI,
-  [1377] = 5,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(112), 1,
+    ACTIONS(154), 1,
       anon_sym_LPAREN,
-    ACTIONS(138), 1,
-      anon_sym_COLON,
-    STATE(80), 1,
-      sym_ascription,
-    STATE(46), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-  [1394] = 4,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(112), 1,
-      anon_sym_LPAREN,
-    ACTIONS(140), 2,
-      anon_sym_EQ_GT,
-      anon_sym_u21d2,
-    STATE(26), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-  [1409] = 5,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(112), 1,
-      anon_sym_LPAREN,
-    ACTIONS(138), 1,
-      anon_sym_COLON,
-    STATE(90), 1,
-      sym_ascription,
-    STATE(26), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-  [1426] = 4,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(112), 1,
-      anon_sym_LPAREN,
-    ACTIONS(142), 2,
-      anon_sym_EQ_GT,
-      anon_sym_u21d2,
-    STATE(26), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-  [1441] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(144), 4,
-      ts_builtin_sym_end,
-      anon_sym_axiom,
-      anon_sym_def,
-      sym_command,
-  [1451] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(146), 4,
-      ts_builtin_sym_end,
-      anon_sym_axiom,
-      anon_sym_def,
-      sym_command,
-  [1461] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(148), 4,
-      ts_builtin_sym_end,
-      anon_sym_axiom,
-      anon_sym_def,
-      sym_command,
-  [1471] = 4,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(150), 1,
-      anon_sym_LPAREN,
-    ACTIONS(153), 1,
+    ACTIONS(157), 1,
       anon_sym_in,
-    STATE(51), 2,
+    STATE(57), 2,
       sym_binding,
       aux_sym_let_repeat1,
-  [1485] = 2,
+  [1800] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(155), 4,
+    ACTIONS(159), 4,
       ts_builtin_sym_end,
       anon_sym_axiom,
       anon_sym_def,
       sym_command,
-  [1495] = 2,
+  [1810] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(157), 4,
+    ACTIONS(161), 4,
       ts_builtin_sym_end,
       anon_sym_axiom,
       anon_sym_def,
       sym_command,
-  [1505] = 4,
+  [1820] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(159), 1,
-      anon_sym_LPAREN,
-    ACTIONS(161), 1,
-      anon_sym_in,
-    STATE(51), 2,
-      sym_binding,
-      aux_sym_let_repeat1,
-  [1519] = 4,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(112), 1,
-      anon_sym_LPAREN,
-    ACTIONS(163), 1,
-      anon_sym_COMMA,
-    STATE(26), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-  [1533] = 2,
+    ACTIONS(163), 4,
+      ts_builtin_sym_end,
+      anon_sym_axiom,
+      anon_sym_def,
+      sym_command,
+  [1830] = 2,
     ACTIONS(3), 1,
       sym_comment,
     ACTIONS(165), 4,
@@ -2149,218 +2395,250 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_axiom,
       anon_sym_def,
       sym_command,
-  [1543] = 4,
+  [1840] = 4,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(112), 1,
-      anon_sym_LPAREN,
     ACTIONS(167), 1,
-      anon_sym_COMMA,
-    STATE(26), 2,
+      anon_sym_LPAREN,
+    ACTIONS(169), 1,
+      anon_sym_in,
+    STATE(57), 2,
+      sym_binding,
+      aux_sym_let_repeat1,
+  [1854] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(171), 4,
+      ts_builtin_sym_end,
+      anon_sym_axiom,
+      anon_sym_def,
+      sym_command,
+  [1864] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(173), 4,
+      ts_builtin_sym_end,
+      anon_sym_axiom,
+      anon_sym_def,
+      sym_command,
+  [1874] = 3,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(126), 1,
+      anon_sym_LPAREN,
+    STATE(51), 2,
       sym_param_block,
       aux_sym_labs_repeat1,
-  [1557] = 3,
+  [1885] = 3,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(112), 1,
+    ACTIONS(126), 1,
       anon_sym_LPAREN,
     STATE(45), 2,
       sym_param_block,
       aux_sym_labs_repeat1,
-  [1568] = 3,
+  [1896] = 3,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(159), 1,
+    ACTIONS(167), 1,
       anon_sym_LPAREN,
-    STATE(54), 2,
+    STATE(62), 2,
       sym_binding,
       aux_sym_let_repeat1,
-  [1579] = 4,
+  [1907] = 3,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(169), 1,
+    ACTIONS(126), 1,
+      anon_sym_LPAREN,
+    STATE(53), 2,
+      sym_param_block,
+      aux_sym_labs_repeat1,
+  [1918] = 4,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(175), 1,
       sym_identifier,
-    ACTIONS(172), 1,
+    ACTIONS(177), 1,
       anon_sym_COLON,
-    STATE(60), 1,
+    STATE(71), 1,
       aux_sym_param_block_repeat1,
-  [1592] = 3,
+  [1931] = 3,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(130), 1,
+    ACTIONS(96), 1,
       anon_sym_end,
-    ACTIONS(174), 2,
+    ACTIONS(179), 2,
       anon_sym_DASH_GT,
       anon_sym_u2192,
-  [1603] = 4,
+  [1942] = 4,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(176), 1,
+    ACTIONS(181), 1,
       sym_identifier,
-    ACTIONS(178), 1,
+    ACTIONS(184), 1,
       anon_sym_COLON,
-    STATE(60), 1,
+    STATE(71), 1,
       aux_sym_param_block_repeat1,
-  [1616] = 3,
+  [1955] = 3,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(112), 1,
+    ACTIONS(126), 1,
       anon_sym_LPAREN,
-    STATE(55), 2,
+    STATE(46), 2,
       sym_param_block,
       aux_sym_labs_repeat1,
-  [1627] = 3,
+  [1966] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(112), 1,
-      anon_sym_LPAREN,
-    STATE(47), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-  [1638] = 3,
+    ACTIONS(186), 2,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+  [1974] = 3,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(112), 1,
-      anon_sym_LPAREN,
-    STATE(57), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-  [1649] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(180), 2,
-      anon_sym_LPAREN,
-      anon_sym_in,
-  [1657] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(182), 2,
-      anon_sym_LPAREN,
-      anon_sym_in,
-  [1665] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(184), 2,
-      anon_sym_COLON_EQ,
-      anon_sym_SEMI,
-  [1673] = 3,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(186), 1,
+    ACTIONS(188), 1,
       sym_identifier,
-    STATE(62), 1,
+    STATE(69), 1,
       aux_sym_param_block_repeat1,
-  [1683] = 2,
+  [1984] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(188), 2,
+    ACTIONS(190), 2,
       anon_sym_LPAREN,
       anon_sym_in,
-  [1691] = 2,
+  [1992] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(190), 1,
-      ts_builtin_sym_end,
-  [1698] = 2,
+    ACTIONS(192), 2,
+      anon_sym_LPAREN,
+      anon_sym_in,
+  [2000] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(192), 1,
-      anon_sym_RPAREN,
-  [1705] = 2,
+    ACTIONS(194), 2,
+      anon_sym_LPAREN,
+      anon_sym_in,
+  [2008] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(134), 1,
-      anon_sym_COLON_EQ,
-  [1712] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(128), 1,
-      anon_sym_COLON_EQ,
-  [1719] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(194), 1,
-      anon_sym_RPAREN,
-  [1726] = 2,
-    ACTIONS(3), 1,
-      sym_comment,
-    ACTIONS(196), 1,
-      anon_sym_RPAREN,
-  [1733] = 2,
+    ACTIONS(196), 2,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+  [2016] = 2,
     ACTIONS(3), 1,
       sym_comment,
     ACTIONS(198), 1,
-      anon_sym_end,
-  [1740] = 2,
+      anon_sym_SEMI,
+  [2023] = 2,
     ACTIONS(3), 1,
       sym_comment,
     ACTIONS(200), 1,
-      sym_identifier,
-  [1747] = 2,
+      anon_sym_RPAREN,
+  [2030] = 2,
     ACTIONS(3), 1,
       sym_comment,
     ACTIONS(202), 1,
       anon_sym_RPAREN,
-  [1754] = 2,
+  [2037] = 2,
     ACTIONS(3), 1,
       sym_comment,
     ACTIONS(204), 1,
       anon_sym_SEMI,
-  [1761] = 2,
+  [2044] = 2,
     ACTIONS(3), 1,
       sym_comment,
     ACTIONS(206), 1,
-      anon_sym_RPAREN,
-  [1768] = 2,
+      ts_builtin_sym_end,
+  [2051] = 2,
     ACTIONS(3), 1,
       sym_comment,
     ACTIONS(208), 1,
-      sym_identifier,
-  [1775] = 2,
+      anon_sym_end,
+  [2058] = 2,
     ACTIONS(3), 1,
       sym_comment,
     ACTIONS(210), 1,
-      anon_sym_SEMI,
-  [1782] = 2,
+      anon_sym_RPAREN,
+  [2065] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(148), 1,
+      anon_sym_COLON_EQ,
+  [2072] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
     ACTIONS(212), 1,
+      anon_sym_COMMA,
+  [2079] = 2,
+    ACTIONS(3), 1,
       sym_comment,
     ACTIONS(214), 1,
-      sym_post_command,
-  [1789] = 2,
+      sym_identifier,
+  [2086] = 2,
     ACTIONS(3), 1,
       sym_comment,
     ACTIONS(216), 1,
-      sym_identifier,
-  [1796] = 2,
+      anon_sym_SEMI,
+  [2093] = 2,
     ACTIONS(3), 1,
       sym_comment,
     ACTIONS(218), 1,
-      anon_sym_RPAREN,
-  [1803] = 2,
+      sym_identifier,
+  [2100] = 2,
     ACTIONS(3), 1,
       sym_comment,
     ACTIONS(220), 1,
-      anon_sym_COLON_EQ,
-  [1810] = 2,
+      anon_sym_RPAREN,
+  [2107] = 2,
     ACTIONS(3), 1,
       sym_comment,
     ACTIONS(222), 1,
       anon_sym_SEMI,
-  [1817] = 2,
+  [2114] = 2,
     ACTIONS(3), 1,
       sym_comment,
     ACTIONS(224), 1,
       anon_sym_COLON_EQ,
-  [1824] = 2,
+  [2121] = 2,
     ACTIONS(3), 1,
       sym_comment,
     ACTIONS(226), 1,
-      anon_sym_SEMI,
-  [1831] = 2,
+      anon_sym_RPAREN,
+  [2128] = 2,
+    ACTIONS(228), 1,
+      sym_comment,
+    ACTIONS(230), 1,
+      sym_post_command,
+  [2135] = 2,
     ACTIONS(3), 1,
       sym_comment,
-    ACTIONS(228), 1,
+    ACTIONS(232), 1,
+      sym_identifier,
+  [2142] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(234), 1,
+      anon_sym_RPAREN,
+  [2149] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(236), 1,
+      anon_sym_COMMA,
+  [2156] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(238), 1,
       anon_sym_SEMI,
+  [2163] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(240), 1,
+      anon_sym_COLON_EQ,
+  [2170] = 2,
+    ACTIONS(3), 1,
+      sym_comment,
+    ACTIONS(144), 1,
+      anon_sym_COLON_EQ,
 };
 
 static const uint32_t ts_small_parse_table_map[] = {
@@ -2382,78 +2660,88 @@ static const uint32_t ts_small_parse_table_map[] = {
   [SMALL_STATE(17)] = 810,
   [SMALL_STATE(18)] = 864,
   [SMALL_STATE(19)] = 918,
-  [SMALL_STATE(20)] = 947,
-  [SMALL_STATE(21)] = 976,
-  [SMALL_STATE(22)] = 1007,
-  [SMALL_STATE(23)] = 1038,
-  [SMALL_STATE(24)] = 1054,
-  [SMALL_STATE(25)] = 1070,
-  [SMALL_STATE(26)] = 1086,
-  [SMALL_STATE(27)] = 1106,
-  [SMALL_STATE(28)] = 1128,
-  [SMALL_STATE(29)] = 1150,
-  [SMALL_STATE(30)] = 1166,
-  [SMALL_STATE(31)] = 1182,
-  [SMALL_STATE(32)] = 1198,
-  [SMALL_STATE(33)] = 1210,
-  [SMALL_STATE(34)] = 1222,
-  [SMALL_STATE(35)] = 1242,
-  [SMALL_STATE(36)] = 1256,
-  [SMALL_STATE(37)] = 1268,
-  [SMALL_STATE(38)] = 1280,
-  [SMALL_STATE(39)] = 1300,
-  [SMALL_STATE(40)] = 1320,
-  [SMALL_STATE(41)] = 1332,
-  [SMALL_STATE(42)] = 1344,
-  [SMALL_STATE(43)] = 1364,
-  [SMALL_STATE(44)] = 1377,
-  [SMALL_STATE(45)] = 1394,
-  [SMALL_STATE(46)] = 1409,
-  [SMALL_STATE(47)] = 1426,
-  [SMALL_STATE(48)] = 1441,
-  [SMALL_STATE(49)] = 1451,
-  [SMALL_STATE(50)] = 1461,
-  [SMALL_STATE(51)] = 1471,
-  [SMALL_STATE(52)] = 1485,
-  [SMALL_STATE(53)] = 1495,
-  [SMALL_STATE(54)] = 1505,
-  [SMALL_STATE(55)] = 1519,
-  [SMALL_STATE(56)] = 1533,
-  [SMALL_STATE(57)] = 1543,
-  [SMALL_STATE(58)] = 1557,
-  [SMALL_STATE(59)] = 1568,
-  [SMALL_STATE(60)] = 1579,
-  [SMALL_STATE(61)] = 1592,
-  [SMALL_STATE(62)] = 1603,
-  [SMALL_STATE(63)] = 1616,
-  [SMALL_STATE(64)] = 1627,
-  [SMALL_STATE(65)] = 1638,
-  [SMALL_STATE(66)] = 1649,
-  [SMALL_STATE(67)] = 1657,
-  [SMALL_STATE(68)] = 1665,
-  [SMALL_STATE(69)] = 1673,
-  [SMALL_STATE(70)] = 1683,
-  [SMALL_STATE(71)] = 1691,
-  [SMALL_STATE(72)] = 1698,
-  [SMALL_STATE(73)] = 1705,
-  [SMALL_STATE(74)] = 1712,
-  [SMALL_STATE(75)] = 1719,
-  [SMALL_STATE(76)] = 1726,
-  [SMALL_STATE(77)] = 1733,
-  [SMALL_STATE(78)] = 1740,
-  [SMALL_STATE(79)] = 1747,
-  [SMALL_STATE(80)] = 1754,
-  [SMALL_STATE(81)] = 1761,
-  [SMALL_STATE(82)] = 1768,
-  [SMALL_STATE(83)] = 1775,
-  [SMALL_STATE(84)] = 1782,
-  [SMALL_STATE(85)] = 1789,
-  [SMALL_STATE(86)] = 1796,
-  [SMALL_STATE(87)] = 1803,
-  [SMALL_STATE(88)] = 1810,
-  [SMALL_STATE(89)] = 1817,
-  [SMALL_STATE(90)] = 1824,
-  [SMALL_STATE(91)] = 1831,
+  [SMALL_STATE(20)] = 972,
+  [SMALL_STATE(21)] = 1026,
+  [SMALL_STATE(22)] = 1080,
+  [SMALL_STATE(23)] = 1134,
+  [SMALL_STATE(24)] = 1166,
+  [SMALL_STATE(25)] = 1198,
+  [SMALL_STATE(26)] = 1217,
+  [SMALL_STATE(27)] = 1236,
+  [SMALL_STATE(28)] = 1255,
+  [SMALL_STATE(29)] = 1286,
+  [SMALL_STATE(30)] = 1317,
+  [SMALL_STATE(31)] = 1332,
+  [SMALL_STATE(32)] = 1347,
+  [SMALL_STATE(33)] = 1362,
+  [SMALL_STATE(34)] = 1377,
+  [SMALL_STATE(35)] = 1392,
+  [SMALL_STATE(36)] = 1407,
+  [SMALL_STATE(37)] = 1422,
+  [SMALL_STATE(38)] = 1437,
+  [SMALL_STATE(39)] = 1459,
+  [SMALL_STATE(40)] = 1479,
+  [SMALL_STATE(41)] = 1495,
+  [SMALL_STATE(42)] = 1511,
+  [SMALL_STATE(43)] = 1527,
+  [SMALL_STATE(44)] = 1549,
+  [SMALL_STATE(45)] = 1565,
+  [SMALL_STATE(46)] = 1586,
+  [SMALL_STATE(47)] = 1607,
+  [SMALL_STATE(48)] = 1627,
+  [SMALL_STATE(49)] = 1641,
+  [SMALL_STATE(50)] = 1661,
+  [SMALL_STATE(51)] = 1681,
+  [SMALL_STATE(52)] = 1701,
+  [SMALL_STATE(53)] = 1721,
+  [SMALL_STATE(54)] = 1741,
+  [SMALL_STATE(55)] = 1752,
+  [SMALL_STATE(56)] = 1769,
+  [SMALL_STATE(57)] = 1786,
+  [SMALL_STATE(58)] = 1800,
+  [SMALL_STATE(59)] = 1810,
+  [SMALL_STATE(60)] = 1820,
+  [SMALL_STATE(61)] = 1830,
+  [SMALL_STATE(62)] = 1840,
+  [SMALL_STATE(63)] = 1854,
+  [SMALL_STATE(64)] = 1864,
+  [SMALL_STATE(65)] = 1874,
+  [SMALL_STATE(66)] = 1885,
+  [SMALL_STATE(67)] = 1896,
+  [SMALL_STATE(68)] = 1907,
+  [SMALL_STATE(69)] = 1918,
+  [SMALL_STATE(70)] = 1931,
+  [SMALL_STATE(71)] = 1942,
+  [SMALL_STATE(72)] = 1955,
+  [SMALL_STATE(73)] = 1966,
+  [SMALL_STATE(74)] = 1974,
+  [SMALL_STATE(75)] = 1984,
+  [SMALL_STATE(76)] = 1992,
+  [SMALL_STATE(77)] = 2000,
+  [SMALL_STATE(78)] = 2008,
+  [SMALL_STATE(79)] = 2016,
+  [SMALL_STATE(80)] = 2023,
+  [SMALL_STATE(81)] = 2030,
+  [SMALL_STATE(82)] = 2037,
+  [SMALL_STATE(83)] = 2044,
+  [SMALL_STATE(84)] = 2051,
+  [SMALL_STATE(85)] = 2058,
+  [SMALL_STATE(86)] = 2065,
+  [SMALL_STATE(87)] = 2072,
+  [SMALL_STATE(88)] = 2079,
+  [SMALL_STATE(89)] = 2086,
+  [SMALL_STATE(90)] = 2093,
+  [SMALL_STATE(91)] = 2100,
+  [SMALL_STATE(92)] = 2107,
+  [SMALL_STATE(93)] = 2114,
+  [SMALL_STATE(94)] = 2121,
+  [SMALL_STATE(95)] = 2128,
+  [SMALL_STATE(96)] = 2135,
+  [SMALL_STATE(97)] = 2142,
+  [SMALL_STATE(98)] = 2149,
+  [SMALL_STATE(99)] = 2156,
+  [SMALL_STATE(100)] = 2163,
+  [SMALL_STATE(101)] = 2170,
 };
 
 static const TSParseActionEntry ts_parse_actions[] = {
@@ -2461,111 +2749,117 @@ static const TSParseActionEntry ts_parse_actions[] = {
   [1] = {.entry = {.count = 1, .reusable = false}}, RECOVER(),
   [3] = {.entry = {.count = 1, .reusable = true}}, SHIFT_EXTRA(),
   [5] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_program, 0, 0, 0),
-  [7] = {.entry = {.count = 1, .reusable = true}}, SHIFT(78),
-  [9] = {.entry = {.count = 1, .reusable = true}}, SHIFT(85),
-  [11] = {.entry = {.count = 1, .reusable = true}}, SHIFT(84),
-  [13] = {.entry = {.count = 1, .reusable = false}}, SHIFT(24),
+  [7] = {.entry = {.count = 1, .reusable = true}}, SHIFT(90),
+  [9] = {.entry = {.count = 1, .reusable = true}}, SHIFT(96),
+  [11] = {.entry = {.count = 1, .reusable = true}}, SHIFT(95),
+  [13] = {.entry = {.count = 1, .reusable = false}}, SHIFT(25),
   [15] = {.entry = {.count = 1, .reusable = true}}, SHIFT(4),
-  [17] = {.entry = {.count = 1, .reusable = true}}, SHIFT(24),
-  [19] = {.entry = {.count = 1, .reusable = true}}, SHIFT(23),
-  [21] = {.entry = {.count = 1, .reusable = true}}, SHIFT(58),
-  [23] = {.entry = {.count = 1, .reusable = false}}, SHIFT(58),
-  [25] = {.entry = {.count = 1, .reusable = true}}, SHIFT(63),
-  [27] = {.entry = {.count = 1, .reusable = false}}, SHIFT(63),
-  [29] = {.entry = {.count = 1, .reusable = false}}, SHIFT(59),
-  [31] = {.entry = {.count = 1, .reusable = false}}, SHIFT(29),
-  [33] = {.entry = {.count = 1, .reusable = true}}, SHIFT(18),
-  [35] = {.entry = {.count = 1, .reusable = true}}, SHIFT(29),
-  [37] = {.entry = {.count = 1, .reusable = true}}, SHIFT(30),
-  [39] = {.entry = {.count = 1, .reusable = true}}, SHIFT(64),
-  [41] = {.entry = {.count = 1, .reusable = false}}, SHIFT(64),
-  [43] = {.entry = {.count = 1, .reusable = true}}, SHIFT(65),
-  [45] = {.entry = {.count = 1, .reusable = false}}, SHIFT(65),
-  [47] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_app, 1, 0, 0),
-  [49] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(24),
-  [52] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(4),
-  [55] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0),
-  [57] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(23),
-  [60] = {.entry = {.count = 2, .reusable = false}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(29),
-  [63] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(18),
-  [66] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(29),
-  [69] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(30),
-  [72] = {.entry = {.count = 1, .reusable = false}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0),
-  [74] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_app, 1, 0, 0),
-  [76] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_square, 1, 0, 0),
-  [78] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_term, 1, 0, 0),
-  [80] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_term, 3, 0, 0),
-  [82] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_labs_repeat1, 2, 0, 0), SHIFT_REPEAT(69),
-  [85] = {.entry = {.count = 1, .reusable = false}}, REDUCE(aux_sym_labs_repeat1, 2, 0, 0),
-  [87] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_labs_repeat1, 2, 0, 0),
-  [89] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_program, 1, 0, 0),
-  [91] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0),
-  [93] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(78),
-  [96] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(85),
-  [99] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(84),
-  [102] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_term, 1, 0, 0),
-  [104] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_square, 1, 0, 0),
-  [106] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_term, 3, 0, 0),
-  [108] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_app_term, 1, 0, 0),
-  [110] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_arrow, 3, 0, 0),
-  [112] = {.entry = {.count = 1, .reusable = true}}, SHIFT(69),
-  [114] = {.entry = {.count = 1, .reusable = false}}, SHIFT(2),
-  [116] = {.entry = {.count = 1, .reusable = true}}, SHIFT(11),
-  [118] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_param_block, 5, 0, 3),
-  [120] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_param_block, 5, 0, 3),
-  [122] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_labs, 4, 0, 0),
-  [124] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_pabs, 4, 0, 0),
-  [126] = {.entry = {.count = 1, .reusable = true}}, SHIFT(3),
-  [128] = {.entry = {.count = 1, .reusable = true}}, SHIFT(12),
-  [130] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_expr, 1, 0, 0),
-  [132] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_let, 5, 0, 0),
-  [134] = {.entry = {.count = 1, .reusable = true}}, SHIFT(5),
-  [136] = {.entry = {.count = 1, .reusable = true}}, SHIFT(6),
-  [138] = {.entry = {.count = 1, .reusable = true}}, SHIFT(2),
-  [140] = {.entry = {.count = 1, .reusable = true}}, SHIFT(9),
-  [142] = {.entry = {.count = 1, .reusable = true}}, SHIFT(16),
-  [144] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_preprocess, 2, 0, 0),
-  [146] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 5, 0, 2),
-  [148] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_axiom, 5, 0, 2),
-  [150] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_let_repeat1, 2, 0, 0), SHIFT_REPEAT(82),
-  [153] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_let_repeat1, 2, 0, 0),
-  [155] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_axiom, 4, 0, 2),
-  [157] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 6, 0, 2),
-  [159] = {.entry = {.count = 1, .reusable = true}}, SHIFT(82),
-  [161] = {.entry = {.count = 1, .reusable = true}}, SHIFT(10),
-  [163] = {.entry = {.count = 1, .reusable = true}}, SHIFT(15),
+  [17] = {.entry = {.count = 1, .reusable = true}}, SHIFT(25),
+  [19] = {.entry = {.count = 1, .reusable = true}}, SHIFT(26),
+  [21] = {.entry = {.count = 1, .reusable = true}}, SHIFT(66),
+  [23] = {.entry = {.count = 1, .reusable = false}}, SHIFT(66),
+  [25] = {.entry = {.count = 1, .reusable = true}}, SHIFT(65),
+  [27] = {.entry = {.count = 1, .reusable = false}}, SHIFT(65),
+  [29] = {.entry = {.count = 1, .reusable = false}}, SHIFT(67),
+  [31] = {.entry = {.count = 1, .reusable = false}}, SHIFT(40),
+  [33] = {.entry = {.count = 1, .reusable = true}}, SHIFT(21),
+  [35] = {.entry = {.count = 1, .reusable = true}}, SHIFT(40),
+  [37] = {.entry = {.count = 1, .reusable = true}}, SHIFT(42),
+  [39] = {.entry = {.count = 1, .reusable = true}}, SHIFT(72),
+  [41] = {.entry = {.count = 1, .reusable = false}}, SHIFT(72),
+  [43] = {.entry = {.count = 1, .reusable = true}}, SHIFT(68),
+  [45] = {.entry = {.count = 1, .reusable = false}}, SHIFT(68),
+  [47] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(25),
+  [50] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(4),
+  [53] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0),
+  [55] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(26),
+  [58] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_app, 1, 0, 0),
+  [60] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_term, 1, 0, 0),
+  [62] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_square, 1, 0, 0),
+  [64] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_term, 3, 0, 0),
+  [66] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_app, 1, 0, 0),
+  [68] = {.entry = {.count = 2, .reusable = false}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(40),
+  [71] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(21),
+  [74] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(40),
+  [77] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(42),
+  [80] = {.entry = {.count = 1, .reusable = false}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0),
+  [82] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_labs, 5, 0, 0),
+  [84] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_pabs, 5, 0, 0),
+  [86] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_arrow, 3, 0, 0),
+  [88] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_pabs, 4, 0, 0),
+  [90] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_labs, 4, 0, 0),
+  [92] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_let, 5, 0, 0),
+  [94] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_app_term, 1, 0, 0),
+  [96] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_expr, 1, 0, 0),
+  [98] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_program, 1, 0, 0),
+  [100] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_labs_repeat1, 2, 0, 0), SHIFT_REPEAT(74),
+  [103] = {.entry = {.count = 1, .reusable = false}}, REDUCE(aux_sym_labs_repeat1, 2, 0, 0),
+  [105] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_labs_repeat1, 2, 0, 0),
+  [107] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_term, 1, 0, 0),
+  [109] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_term, 3, 0, 0),
+  [111] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_square, 1, 0, 0),
+  [113] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0),
+  [115] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(90),
+  [118] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(96),
+  [121] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(95),
+  [124] = {.entry = {.count = 1, .reusable = true}}, SHIFT(7),
+  [126] = {.entry = {.count = 1, .reusable = true}}, SHIFT(74),
+  [128] = {.entry = {.count = 1, .reusable = true}}, SHIFT(10),
+  [130] = {.entry = {.count = 1, .reusable = true}}, SHIFT(2),
+  [132] = {.entry = {.count = 1, .reusable = true}}, SHIFT(17),
+  [134] = {.entry = {.count = 1, .reusable = false}}, SHIFT(10),
+  [136] = {.entry = {.count = 1, .reusable = true}}, SHIFT(13),
+  [138] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_param_block, 5, 0, 3),
+  [140] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_param_block, 5, 0, 3),
+  [142] = {.entry = {.count = 1, .reusable = true}}, SHIFT(3),
+  [144] = {.entry = {.count = 1, .reusable = true}}, SHIFT(14),
+  [146] = {.entry = {.count = 1, .reusable = true}}, SHIFT(9),
+  [148] = {.entry = {.count = 1, .reusable = true}}, SHIFT(5),
+  [150] = {.entry = {.count = 1, .reusable = true}}, SHIFT(18),
+  [152] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_ascription, 2, 0, 1),
+  [154] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_let_repeat1, 2, 0, 0), SHIFT_REPEAT(88),
+  [157] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_let_repeat1, 2, 0, 0),
+  [159] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_preprocess, 2, 0, 0),
+  [161] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 6, 0, 2),
+  [163] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_axiom, 4, 0, 2),
   [165] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 7, 0, 2),
-  [167] = {.entry = {.count = 1, .reusable = true}}, SHIFT(17),
-  [169] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_param_block_repeat1, 2, 0, 0), SHIFT_REPEAT(60),
-  [172] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_param_block_repeat1, 2, 0, 0),
-  [174] = {.entry = {.count = 1, .reusable = true}}, SHIFT(14),
-  [176] = {.entry = {.count = 1, .reusable = true}}, SHIFT(60),
-  [178] = {.entry = {.count = 1, .reusable = true}}, SHIFT(7),
-  [180] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_binding, 5, 0, 0),
-  [182] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_binding, 6, 0, 0),
-  [184] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_ascription, 2, 0, 1),
-  [186] = {.entry = {.count = 1, .reusable = true}}, SHIFT(62),
-  [188] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_binding, 7, 0, 0),
-  [190] = {.entry = {.count = 1, .reusable = true}},  ACCEPT_INPUT(),
-  [192] = {.entry = {.count = 1, .reusable = true}}, SHIFT(67),
-  [194] = {.entry = {.count = 1, .reusable = true}}, SHIFT(70),
-  [196] = {.entry = {.count = 1, .reusable = true}}, SHIFT(25),
-  [198] = {.entry = {.count = 1, .reusable = true}}, SHIFT(41),
-  [200] = {.entry = {.count = 1, .reusable = true}}, SHIFT(44),
-  [202] = {.entry = {.count = 1, .reusable = true}}, SHIFT(35),
-  [204] = {.entry = {.count = 1, .reusable = true}}, SHIFT(52),
-  [206] = {.entry = {.count = 1, .reusable = true}}, SHIFT(66),
-  [208] = {.entry = {.count = 1, .reusable = true}}, SHIFT(34),
-  [210] = {.entry = {.count = 1, .reusable = true}}, SHIFT(49),
-  [212] = {.entry = {.count = 1, .reusable = false}}, SHIFT_EXTRA(),
-  [214] = {.entry = {.count = 1, .reusable = false}}, SHIFT(48),
-  [216] = {.entry = {.count = 1, .reusable = true}}, SHIFT(38),
-  [218] = {.entry = {.count = 1, .reusable = true}}, SHIFT(31),
-  [220] = {.entry = {.count = 1, .reusable = true}}, SHIFT(13),
-  [222] = {.entry = {.count = 1, .reusable = true}}, SHIFT(56),
-  [224] = {.entry = {.count = 1, .reusable = true}}, SHIFT(8),
-  [226] = {.entry = {.count = 1, .reusable = true}}, SHIFT(50),
-  [228] = {.entry = {.count = 1, .reusable = true}}, SHIFT(53),
+  [167] = {.entry = {.count = 1, .reusable = true}}, SHIFT(88),
+  [169] = {.entry = {.count = 1, .reusable = true}}, SHIFT(22),
+  [171] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_axiom, 5, 0, 2),
+  [173] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 5, 0, 2),
+  [175] = {.entry = {.count = 1, .reusable = true}}, SHIFT(71),
+  [177] = {.entry = {.count = 1, .reusable = true}}, SHIFT(6),
+  [179] = {.entry = {.count = 1, .reusable = true}}, SHIFT(16),
+  [181] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_param_block_repeat1, 2, 0, 0), SHIFT_REPEAT(71),
+  [184] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_param_block_repeat1, 2, 0, 0),
+  [186] = {.entry = {.count = 1, .reusable = true}}, SHIFT(11),
+  [188] = {.entry = {.count = 1, .reusable = true}}, SHIFT(69),
+  [190] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_binding, 5, 0, 0),
+  [192] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_binding, 6, 0, 0),
+  [194] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_binding, 7, 0, 0),
+  [196] = {.entry = {.count = 1, .reusable = true}}, SHIFT(19),
+  [198] = {.entry = {.count = 1, .reusable = true}}, SHIFT(60),
+  [200] = {.entry = {.count = 1, .reusable = true}}, SHIFT(48),
+  [202] = {.entry = {.count = 1, .reusable = true}}, SHIFT(77),
+  [204] = {.entry = {.count = 1, .reusable = true}}, SHIFT(61),
+  [206] = {.entry = {.count = 1, .reusable = true}},  ACCEPT_INPUT(),
+  [208] = {.entry = {.count = 1, .reusable = true}}, SHIFT(35),
+  [210] = {.entry = {.count = 1, .reusable = true}}, SHIFT(27),
+  [212] = {.entry = {.count = 1, .reusable = true}}, SHIFT(12),
+  [214] = {.entry = {.count = 1, .reusable = true}}, SHIFT(47),
+  [216] = {.entry = {.count = 1, .reusable = true}}, SHIFT(63),
+  [218] = {.entry = {.count = 1, .reusable = true}}, SHIFT(55),
+  [220] = {.entry = {.count = 1, .reusable = true}}, SHIFT(75),
+  [222] = {.entry = {.count = 1, .reusable = true}}, SHIFT(64),
+  [224] = {.entry = {.count = 1, .reusable = true}}, SHIFT(15),
+  [226] = {.entry = {.count = 1, .reusable = true}}, SHIFT(41),
+  [228] = {.entry = {.count = 1, .reusable = false}}, SHIFT_EXTRA(),
+  [230] = {.entry = {.count = 1, .reusable = false}}, SHIFT(58),
+  [232] = {.entry = {.count = 1, .reusable = true}}, SHIFT(49),
+  [234] = {.entry = {.count = 1, .reusable = true}}, SHIFT(76),
+  [236] = {.entry = {.count = 1, .reusable = true}}, SHIFT(20),
+  [238] = {.entry = {.count = 1, .reusable = true}}, SHIFT(59),
+  [240] = {.entry = {.count = 1, .reusable = true}}, SHIFT(8),
 };
 
 #ifdef __cplusplus
diff --git a/test/corpus/labs.txt b/test/corpus/labs.txt
index 17a56f0..a2ad2c1 100644
--- a/test/corpus/labs.txt
+++ b/test/corpus/labs.txt
@@ -2,7 +2,7 @@
 Lambda Abstraction
 ==================
 
-def foo := fun (A : *) (x : A) => x;
+def foo := fun (A : *) (x : A) : A => x;
 
 ----------
 
@@ -26,6 +26,12 @@ def foo := fun (A : *) (x : A) => x;
                 (app
                   (term
                     (identifier))))))
+          (ascription
+            (expr
+              (app_term
+                (app
+                  (term
+                    (identifier))))))
           (expr
             (app_term
               (app