From 356b6600f26927efbe71c80564bffb3691212a60 Mon Sep 17 00:00:00 2001
From: William Ball <williampi103@gmail.com>
Date: Sat, 23 Nov 2024 10:06:53 -0800
Subject: [PATCH] added let expressions

---
 grammar.js          |   17 +
 src/grammar.json    |   57 +
 src/node-types.json |   54 +
 src/parser.c        | 2680 ++++++++++++++++++++++++++++---------------
 test/corpus/let.txt |   37 +
 5 files changed, 1921 insertions(+), 924 deletions(-)
 create mode 100644 test/corpus/let.txt

diff --git a/grammar.js b/grammar.js
index 386aec5..3536731 100644
--- a/grammar.js
+++ b/grammar.js
@@ -68,6 +68,22 @@ module.exports = grammar({
       seq('(', $.expr, ')'),
     ),
 
+    binding : $ => seq(
+      '(',
+      $.identifier,
+      ':=',
+      $.expr,
+      ')',
+    ),
+
+    let : $ => seq(
+      'let',
+      repeat1($.binding),
+      'in',
+      $.expr,
+      'end',
+    ),
+
     app : $ => repeat1($.term),
 
     axiom : $ => 'axiom',
@@ -81,6 +97,7 @@ module.exports = grammar({
     app_term : $ => choice(
       $.labs,
       $.pabs,
+      $.let,
       $.app,
     ),
 
diff --git a/src/grammar.json b/src/grammar.json
index ea2bef3..67c06b9 100644
--- a/src/grammar.json
+++ b/src/grammar.json
@@ -243,6 +243,59 @@
         }
       ]
     },
+    "binding": {
+      "type": "SEQ",
+      "members": [
+        {
+          "type": "STRING",
+          "value": "("
+        },
+        {
+          "type": "SYMBOL",
+          "name": "identifier"
+        },
+        {
+          "type": "STRING",
+          "value": ":="
+        },
+        {
+          "type": "SYMBOL",
+          "name": "expr"
+        },
+        {
+          "type": "STRING",
+          "value": ")"
+        }
+      ]
+    },
+    "let": {
+      "type": "SEQ",
+      "members": [
+        {
+          "type": "STRING",
+          "value": "let"
+        },
+        {
+          "type": "REPEAT1",
+          "content": {
+            "type": "SYMBOL",
+            "name": "binding"
+          }
+        },
+        {
+          "type": "STRING",
+          "value": "in"
+        },
+        {
+          "type": "SYMBOL",
+          "name": "expr"
+        },
+        {
+          "type": "STRING",
+          "value": "end"
+        }
+      ]
+    },
     "app": {
       "type": "REPEAT1",
       "content": {
@@ -295,6 +348,10 @@
           "type": "SYMBOL",
           "name": "pabs"
         },
+        {
+          "type": "SYMBOL",
+          "name": "let"
+        },
         {
           "type": "SYMBOL",
           "name": "app"
diff --git a/src/node-types.json b/src/node-types.json
index 667aa6e..03942ae 100644
--- a/src/node-types.json
+++ b/src/node-types.json
@@ -30,6 +30,10 @@
           "type": "labs",
           "named": true
         },
+        {
+          "type": "let",
+          "named": true
+        },
         {
           "type": "pabs",
           "named": true
@@ -72,6 +76,25 @@
       }
     }
   },
+  {
+    "type": "binding",
+    "named": true,
+    "fields": {},
+    "children": {
+      "multiple": true,
+      "required": true,
+      "types": [
+        {
+          "type": "expr",
+          "named": true
+        },
+        {
+          "type": "identifier",
+          "named": true
+        }
+      ]
+    }
+  },
   {
     "type": "definition",
     "named": true,
@@ -148,6 +171,25 @@
       ]
     }
   },
+  {
+    "type": "let",
+    "named": true,
+    "fields": {},
+    "children": {
+      "multiple": true,
+      "required": true,
+      "types": [
+        {
+          "type": "binding",
+          "named": true
+        },
+        {
+          "type": "expr",
+          "named": true
+        }
+      ]
+    }
+  },
   {
     "type": "pabs",
     "named": true,
@@ -315,6 +357,10 @@
     "type": "comment",
     "named": true
   },
+  {
+    "type": "end",
+    "named": false
+  },
   {
     "type": "forall",
     "named": false
@@ -327,6 +373,14 @@
     "type": "identifier",
     "named": true
   },
+  {
+    "type": "in",
+    "named": false
+  },
+  {
+    "type": "let",
+    "named": false
+  },
   {
     "type": "post_command",
     "named": true
diff --git a/src/parser.c b/src/parser.c
index 7d64438..82b0c03 100644
--- a/src/parser.c
+++ b/src/parser.c
@@ -5,11 +5,11 @@
 #endif
 
 #define LANGUAGE_VERSION 14
-#define STATE_COUNT 52
-#define LARGE_STATE_COUNT 5
-#define SYMBOL_COUNT 41
+#define STATE_COUNT 78
+#define LARGE_STATE_COUNT 2
+#define SYMBOL_COUNT 47
 #define ALIAS_COUNT 0
-#define TOKEN_COUNT 24
+#define TOKEN_COUNT 27
 #define EXTERNAL_TOKEN_COUNT 0
 #define FIELD_COUNT 3
 #define MAX_ALIAS_SEQUENCE_LENGTH 6
@@ -32,30 +32,36 @@ enum ts_symbol_identifiers {
   anon_sym_u220f = 14,
   anon_sym_forall = 15,
   anon_sym_COMMA = 16,
-  sym_axiom = 17,
-  anon_sym_DASH_GT = 18,
-  anon_sym_u2192 = 19,
-  anon_sym_COLON_EQ = 20,
-  anon_sym_SEMI = 21,
-  sym_post_command = 22,
-  sym_command = 23,
-  sym_program = 24,
-  sym_param_block = 25,
-  sym_square = 26,
-  sym_labs = 27,
-  sym_pabs = 28,
-  sym_term = 29,
-  sym_app = 30,
-  sym_arrow = 31,
-  sym_app_term = 32,
-  sym_expr = 33,
-  sym_ascription = 34,
-  sym_definition = 35,
-  sym_preprocess = 36,
-  aux_sym_program_repeat1 = 37,
-  aux_sym_param_block_repeat1 = 38,
-  aux_sym_labs_repeat1 = 39,
-  aux_sym_app_repeat1 = 40,
+  anon_sym_COLON_EQ = 17,
+  anon_sym_let = 18,
+  anon_sym_in = 19,
+  anon_sym_end = 20,
+  sym_axiom = 21,
+  anon_sym_DASH_GT = 22,
+  anon_sym_u2192 = 23,
+  anon_sym_SEMI = 24,
+  sym_post_command = 25,
+  sym_command = 26,
+  sym_program = 27,
+  sym_param_block = 28,
+  sym_square = 29,
+  sym_labs = 30,
+  sym_pabs = 31,
+  sym_term = 32,
+  sym_binding = 33,
+  sym_let = 34,
+  sym_app = 35,
+  sym_arrow = 36,
+  sym_app_term = 37,
+  sym_expr = 38,
+  sym_ascription = 39,
+  sym_definition = 40,
+  sym_preprocess = 41,
+  aux_sym_program_repeat1 = 42,
+  aux_sym_param_block_repeat1 = 43,
+  aux_sym_labs_repeat1 = 44,
+  aux_sym_let_repeat1 = 45,
+  aux_sym_app_repeat1 = 46,
 };
 
 static const char * const ts_symbol_names[] = {
@@ -76,10 +82,13 @@ static const char * const ts_symbol_names[] = {
   [anon_sym_u220f] = "\u220f",
   [anon_sym_forall] = "forall",
   [anon_sym_COMMA] = ",",
+  [anon_sym_COLON_EQ] = ":=",
+  [anon_sym_let] = "let",
+  [anon_sym_in] = "in",
+  [anon_sym_end] = "end",
   [sym_axiom] = "axiom",
   [anon_sym_DASH_GT] = "->",
   [anon_sym_u2192] = "\u2192",
-  [anon_sym_COLON_EQ] = ":=",
   [anon_sym_SEMI] = ";",
   [sym_post_command] = "post_command",
   [sym_command] = "command",
@@ -89,6 +98,8 @@ static const char * const ts_symbol_names[] = {
   [sym_labs] = "labs",
   [sym_pabs] = "pabs",
   [sym_term] = "term",
+  [sym_binding] = "binding",
+  [sym_let] = "let",
   [sym_app] = "app",
   [sym_arrow] = "arrow",
   [sym_app_term] = "app_term",
@@ -99,6 +110,7 @@ static const char * const ts_symbol_names[] = {
   [aux_sym_program_repeat1] = "program_repeat1",
   [aux_sym_param_block_repeat1] = "param_block_repeat1",
   [aux_sym_labs_repeat1] = "labs_repeat1",
+  [aux_sym_let_repeat1] = "let_repeat1",
   [aux_sym_app_repeat1] = "app_repeat1",
 };
 
@@ -120,10 +132,13 @@ static const TSSymbol ts_symbol_map[] = {
   [anon_sym_u220f] = anon_sym_u220f,
   [anon_sym_forall] = anon_sym_forall,
   [anon_sym_COMMA] = anon_sym_COMMA,
+  [anon_sym_COLON_EQ] = anon_sym_COLON_EQ,
+  [anon_sym_let] = anon_sym_let,
+  [anon_sym_in] = anon_sym_in,
+  [anon_sym_end] = anon_sym_end,
   [sym_axiom] = sym_axiom,
   [anon_sym_DASH_GT] = anon_sym_DASH_GT,
   [anon_sym_u2192] = anon_sym_u2192,
-  [anon_sym_COLON_EQ] = anon_sym_COLON_EQ,
   [anon_sym_SEMI] = anon_sym_SEMI,
   [sym_post_command] = sym_post_command,
   [sym_command] = sym_command,
@@ -133,6 +148,8 @@ static const TSSymbol ts_symbol_map[] = {
   [sym_labs] = sym_labs,
   [sym_pabs] = sym_pabs,
   [sym_term] = sym_term,
+  [sym_binding] = sym_binding,
+  [sym_let] = sym_let,
   [sym_app] = sym_app,
   [sym_arrow] = sym_arrow,
   [sym_app_term] = sym_app_term,
@@ -143,6 +160,7 @@ static const TSSymbol ts_symbol_map[] = {
   [aux_sym_program_repeat1] = aux_sym_program_repeat1,
   [aux_sym_param_block_repeat1] = aux_sym_param_block_repeat1,
   [aux_sym_labs_repeat1] = aux_sym_labs_repeat1,
+  [aux_sym_let_repeat1] = aux_sym_let_repeat1,
   [aux_sym_app_repeat1] = aux_sym_app_repeat1,
 };
 
@@ -215,6 +233,22 @@ static const TSSymbolMetadata ts_symbol_metadata[] = {
     .visible = true,
     .named = false,
   },
+  [anon_sym_COLON_EQ] = {
+    .visible = true,
+    .named = false,
+  },
+  [anon_sym_let] = {
+    .visible = true,
+    .named = false,
+  },
+  [anon_sym_in] = {
+    .visible = true,
+    .named = false,
+  },
+  [anon_sym_end] = {
+    .visible = true,
+    .named = false,
+  },
   [sym_axiom] = {
     .visible = true,
     .named = true,
@@ -227,10 +261,6 @@ static const TSSymbolMetadata ts_symbol_metadata[] = {
     .visible = true,
     .named = false,
   },
-  [anon_sym_COLON_EQ] = {
-    .visible = true,
-    .named = false,
-  },
   [anon_sym_SEMI] = {
     .visible = true,
     .named = false,
@@ -267,6 +297,14 @@ static const TSSymbolMetadata ts_symbol_metadata[] = {
     .visible = true,
     .named = true,
   },
+  [sym_binding] = {
+    .visible = true,
+    .named = true,
+  },
+  [sym_let] = {
+    .visible = true,
+    .named = true,
+  },
   [sym_app] = {
     .visible = true,
     .named = true,
@@ -307,6 +345,10 @@ static const TSSymbolMetadata ts_symbol_metadata[] = {
     .visible = false,
     .named = false,
   },
+  [aux_sym_let_repeat1] = {
+    .visible = false,
+    .named = false,
+  },
   [aux_sym_app_repeat1] = {
     .visible = false,
     .named = false,
@@ -368,21 +410,21 @@ static const TSStateId ts_primary_state_ids[STATE_COUNT] = {
   [11] = 11,
   [12] = 12,
   [13] = 13,
-  [14] = 14,
-  [15] = 15,
-  [16] = 16,
-  [17] = 17,
+  [14] = 8,
+  [15] = 12,
+  [16] = 10,
+  [17] = 7,
   [18] = 18,
   [19] = 19,
-  [20] = 20,
-  [21] = 21,
+  [20] = 19,
+  [21] = 18,
   [22] = 22,
   [23] = 23,
   [24] = 24,
   [25] = 25,
-  [26] = 26,
-  [27] = 27,
-  [28] = 28,
+  [26] = 24,
+  [27] = 22,
+  [28] = 23,
   [29] = 29,
   [30] = 30,
   [31] = 31,
@@ -397,15 +439,41 @@ static const TSStateId ts_primary_state_ids[STATE_COUNT] = {
   [40] = 40,
   [41] = 41,
   [42] = 42,
-  [43] = 43,
+  [43] = 41,
   [44] = 44,
   [45] = 45,
   [46] = 46,
-  [47] = 47,
+  [47] = 44,
   [48] = 48,
   [49] = 49,
   [50] = 50,
   [51] = 51,
+  [52] = 52,
+  [53] = 53,
+  [54] = 54,
+  [55] = 55,
+  [56] = 56,
+  [57] = 42,
+  [58] = 58,
+  [59] = 54,
+  [60] = 48,
+  [61] = 61,
+  [62] = 62,
+  [63] = 63,
+  [64] = 64,
+  [65] = 65,
+  [66] = 66,
+  [67] = 67,
+  [68] = 68,
+  [69] = 69,
+  [70] = 70,
+  [71] = 71,
+  [72] = 72,
+  [73] = 73,
+  [74] = 68,
+  [75] = 75,
+  [76] = 76,
+  [77] = 77,
 };
 
 static bool ts_lex(TSLexer *lexer, TSStateId state) {
@@ -413,350 +481,494 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) {
   eof = lexer->eof(lexer);
   switch (state) {
     case 0:
-      if (eof) ADVANCE(18);
+      if (eof) ADVANCE(35);
       ADVANCE_MAP(
-        '(', 33,
-        ')', 35,
-        '*', 36,
-        ',', 45,
-        '-', 6,
-        ':', 34,
-        ';', 50,
-        '=', 7,
-        '@', 12,
-        '[', 3,
-        'a', 28,
-        'f', 25,
-        0x3bb, 39,
-        0x2192, 48,
-        0x21d2, 42,
-        0x220f, 43,
-        0x25a1, 37,
+        '(', 54,
+        ')', 56,
+        '*', 57,
+        ',', 68,
+        '-', 8,
+        ':', 55,
+        ';', 79,
+        '=', 9,
+        '@', 18,
+        '[', 5,
+        'a', 32,
+        'e', 23,
+        'f', 27,
+        'i', 24,
+        'l', 15,
+        0x3bb, 60,
+        0x2192, 78,
+        0x21d2, 64,
+        0x220f, 65,
+        0x25a1, 58,
       );
       if (('\t' <= lookahead && lookahead <= '\r') ||
           lookahead == ' ') SKIP(0);
-      if (('A' <= lookahead && lookahead <= 'Z') ||
-          lookahead == '_' ||
-          ('b' <= lookahead && lookahead <= 'z')) ADVANCE(29);
       END_STATE();
     case 1:
       if (lookahead == '\n') SKIP(1);
-      if (lookahead == '-') ADVANCE(55);
-      if (lookahead == '[') ADVANCE(54);
+      if (lookahead == '-') ADVANCE(84);
+      if (lookahead == '[') ADVANCE(83);
       if (('\t' <= lookahead && lookahead <= '\r') ||
-          lookahead == ' ') ADVANCE(56);
-      if (lookahead != 0) ADVANCE(57);
+          lookahead == ' ') ADVANCE(85);
+      if (lookahead != 0) ADVANCE(86);
       END_STATE();
     case 2:
-      ADVANCE_MAP(
-        '(', 33,
-        '*', 36,
-        '-', 5,
-        '[', 3,
-        'f', 25,
-        0x3bb, 39,
-        0x220f, 43,
-        0x25a1, 37,
-      );
+      if (lookahead == '(') ADVANCE(54);
+      if (lookahead == '*') ADVANCE(57);
+      if (lookahead == '-') ADVANCE(8);
+      if (lookahead == '[') ADVANCE(5);
+      if (lookahead == 'e') ADVANCE(44);
+      if (lookahead == 0x2192) ADVANCE(78);
+      if (lookahead == 0x25a1) ADVANCE(58);
       if (('\t' <= lookahead && lookahead <= '\r') ||
           lookahead == ' ') SKIP(2);
       if (('A' <= lookahead && lookahead <= 'Z') ||
           lookahead == '_' ||
-          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(29);
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50);
       END_STATE();
     case 3:
-      if (lookahead == '*') ADVANCE(4);
-      if (lookahead == ']') ADVANCE(38);
-      END_STATE();
-    case 4:
-      if (lookahead == '*') ADVANCE(8);
-      if (lookahead == '[') ADVANCE(16);
-      if (lookahead != 0 &&
-          lookahead != ']') ADVANCE(4);
-      END_STATE();
-    case 5:
-      if (lookahead == '-') ADVANCE(30);
-      END_STATE();
-    case 6:
-      if (lookahead == '-') ADVANCE(30);
-      if (lookahead == '>') ADVANCE(47);
-      END_STATE();
-    case 7:
-      if (lookahead == '>') ADVANCE(41);
-      END_STATE();
-    case 8:
-      if (lookahead == ']') ADVANCE(32);
-      if (lookahead != 0) ADVANCE(4);
-      END_STATE();
-    case 9:
-      if (lookahead == 'c') ADVANCE(13);
-      END_STATE();
-    case 10:
-      if (lookahead == 'd') ADVANCE(11);
-      END_STATE();
-    case 11:
-      if (lookahead == 'e') ADVANCE(58);
-      END_STATE();
-    case 12:
-      if (lookahead == 'i') ADVANCE(14);
-      END_STATE();
-    case 13:
-      if (lookahead == 'l') ADVANCE(15);
-      END_STATE();
-    case 14:
-      if (lookahead == 'n') ADVANCE(9);
-      END_STATE();
-    case 15:
-      if (lookahead == 'u') ADVANCE(10);
-      END_STATE();
-    case 16:
-      if (lookahead != 0) ADVANCE(4);
-      END_STATE();
-    case 17:
-      if (eof) ADVANCE(18);
       ADVANCE_MAP(
-        '(', 33,
-        ')', 35,
-        '*', 36,
-        '-', 6,
-        ':', 34,
-        ';', 50,
-        '@', 12,
-        '[', 3,
-        0x2192, 48,
-        0x25a1, 37,
+        '(', 54,
+        '*', 57,
+        '-', 7,
+        '[', 5,
+        'a', 49,
+        'f', 45,
+        'l', 38,
+        0x3bb, 60,
+        0x220f, 65,
+        0x25a1, 58,
       );
       if (('\t' <= lookahead && lookahead <= '\r') ||
-          lookahead == ' ') SKIP(17);
+          lookahead == ' ') SKIP(3);
       if (('A' <= lookahead && lookahead <= 'Z') ||
           lookahead == '_' ||
-          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(29);
+          ('b' <= lookahead && lookahead <= 'z')) ADVANCE(50);
+      END_STATE();
+    case 4:
+      ADVANCE_MAP(
+        '(', 54,
+        '*', 57,
+        '-', 7,
+        '[', 5,
+        'f', 45,
+        'l', 38,
+        0x3bb, 60,
+        0x220f, 65,
+        0x25a1, 58,
+      );
+      if (('\t' <= lookahead && lookahead <= '\r') ||
+          lookahead == ' ') SKIP(4);
+      if (('A' <= lookahead && lookahead <= 'Z') ||
+          lookahead == '_' ||
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50);
+      END_STATE();
+    case 5:
+      if (lookahead == '*') ADVANCE(6);
+      if (lookahead == ']') ADVANCE(59);
+      END_STATE();
+    case 6:
+      if (lookahead == '*') ADVANCE(10);
+      if (lookahead == '[') ADVANCE(33);
+      if (lookahead != 0 &&
+          lookahead != ']') ADVANCE(6);
+      END_STATE();
+    case 7:
+      if (lookahead == '-') ADVANCE(51);
+      END_STATE();
+    case 8:
+      if (lookahead == '-') ADVANCE(51);
+      if (lookahead == '>') ADVANCE(77);
+      END_STATE();
+    case 9:
+      if (lookahead == '>') ADVANCE(63);
+      END_STATE();
+    case 10:
+      if (lookahead == ']') ADVANCE(53);
+      if (lookahead != 0) ADVANCE(6);
+      END_STATE();
+    case 11:
+      if (lookahead == 'a') ADVANCE(21);
+      END_STATE();
+    case 12:
+      if (lookahead == 'c') ADVANCE(19);
+      END_STATE();
+    case 13:
+      if (lookahead == 'd') ADVANCE(73);
+      END_STATE();
+    case 14:
+      if (lookahead == 'd') ADVANCE(16);
+      END_STATE();
+    case 15:
+      if (lookahead == 'e') ADVANCE(30);
+      END_STATE();
+    case 16:
+      if (lookahead == 'e') ADVANCE(87);
+      END_STATE();
+    case 17:
+      if (lookahead == 'i') ADVANCE(28);
       END_STATE();
     case 18:
-      ACCEPT_TOKEN(ts_builtin_sym_end);
+      if (lookahead == 'i') ADVANCE(25);
       END_STATE();
     case 19:
-      ACCEPT_TOKEN(sym_identifier);
-      if (lookahead == 'a') ADVANCE(22);
-      if (('0' <= lookahead && lookahead <= '9') ||
-          ('A' <= lookahead && lookahead <= 'Z') ||
-          lookahead == '_' ||
-          ('b' <= lookahead && lookahead <= 'z')) ADVANCE(29);
+      if (lookahead == 'l') ADVANCE(31);
       END_STATE();
     case 20:
-      ACCEPT_TOKEN(sym_identifier);
-      if (lookahead == 'i') ADVANCE(26);
-      if (('0' <= lookahead && lookahead <= '9') ||
-          ('A' <= lookahead && lookahead <= 'Z') ||
-          lookahead == '_' ||
-          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(29);
+      if (lookahead == 'l') ADVANCE(66);
       END_STATE();
     case 21:
-      ACCEPT_TOKEN(sym_identifier);
-      if (lookahead == 'l') ADVANCE(44);
-      if (('0' <= lookahead && lookahead <= '9') ||
-          ('A' <= lookahead && lookahead <= 'Z') ||
-          lookahead == '_' ||
-          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(29);
+      if (lookahead == 'l') ADVANCE(20);
       END_STATE();
     case 22:
-      ACCEPT_TOKEN(sym_identifier);
-      if (lookahead == 'l') ADVANCE(21);
-      if (('0' <= lookahead && lookahead <= '9') ||
-          ('A' <= lookahead && lookahead <= 'Z') ||
-          lookahead == '_' ||
-          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(29);
+      if (lookahead == 'm') ADVANCE(75);
       END_STATE();
     case 23:
-      ACCEPT_TOKEN(sym_identifier);
-      if (lookahead == 'm') ADVANCE(46);
-      if (('0' <= lookahead && lookahead <= '9') ||
-          ('A' <= lookahead && lookahead <= 'Z') ||
-          lookahead == '_' ||
-          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(29);
+      if (lookahead == 'n') ADVANCE(13);
       END_STATE();
     case 24:
-      ACCEPT_TOKEN(sym_identifier);
-      if (lookahead == 'n') ADVANCE(40);
-      if (('0' <= lookahead && lookahead <= '9') ||
-          ('A' <= lookahead && lookahead <= 'Z') ||
-          lookahead == '_' ||
-          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(29);
+      if (lookahead == 'n') ADVANCE(72);
       END_STATE();
     case 25:
-      ACCEPT_TOKEN(sym_identifier);
-      if (lookahead == 'o') ADVANCE(27);
-      if (lookahead == 'u') ADVANCE(24);
-      if (('0' <= lookahead && lookahead <= '9') ||
-          ('A' <= lookahead && lookahead <= 'Z') ||
-          lookahead == '_' ||
-          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(29);
+      if (lookahead == 'n') ADVANCE(12);
       END_STATE();
     case 26:
-      ACCEPT_TOKEN(sym_identifier);
-      if (lookahead == 'o') ADVANCE(23);
-      if (('0' <= lookahead && lookahead <= '9') ||
-          ('A' <= lookahead && lookahead <= 'Z') ||
-          lookahead == '_' ||
-          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(29);
+      if (lookahead == 'n') ADVANCE(61);
       END_STATE();
     case 27:
-      ACCEPT_TOKEN(sym_identifier);
-      if (lookahead == 'r') ADVANCE(19);
-      if (('0' <= lookahead && lookahead <= '9') ||
-          ('A' <= lookahead && lookahead <= 'Z') ||
-          lookahead == '_' ||
-          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(29);
+      if (lookahead == 'o') ADVANCE(29);
+      if (lookahead == 'u') ADVANCE(26);
       END_STATE();
     case 28:
-      ACCEPT_TOKEN(sym_identifier);
-      if (lookahead == 'x') ADVANCE(20);
-      if (('0' <= lookahead && lookahead <= '9') ||
-          ('A' <= lookahead && lookahead <= 'Z') ||
-          lookahead == '_' ||
-          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(29);
+      if (lookahead == 'o') ADVANCE(22);
       END_STATE();
     case 29:
+      if (lookahead == 'r') ADVANCE(11);
+      END_STATE();
+    case 30:
+      if (lookahead == 't') ADVANCE(70);
+      END_STATE();
+    case 31:
+      if (lookahead == 'u') ADVANCE(14);
+      END_STATE();
+    case 32:
+      if (lookahead == 'x') ADVANCE(17);
+      END_STATE();
+    case 33:
+      if (lookahead != 0) ADVANCE(6);
+      END_STATE();
+    case 34:
+      if (eof) ADVANCE(35);
+      ADVANCE_MAP(
+        '(', 54,
+        ')', 56,
+        '*', 57,
+        '-', 8,
+        ':', 55,
+        ';', 79,
+        '@', 18,
+        '[', 5,
+        0x2192, 78,
+        0x25a1, 58,
+      );
+      if (('\t' <= lookahead && lookahead <= '\r') ||
+          lookahead == ' ') SKIP(34);
+      if (('A' <= lookahead && lookahead <= 'Z') ||
+          lookahead == '_' ||
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50);
+      END_STATE();
+    case 35:
+      ACCEPT_TOKEN(ts_builtin_sym_end);
+      END_STATE();
+    case 36:
+      ACCEPT_TOKEN(sym_identifier);
+      if (lookahead == 'a') ADVANCE(41);
+      if (('0' <= lookahead && lookahead <= '9') ||
+          ('A' <= lookahead && lookahead <= 'Z') ||
+          lookahead == '_' ||
+          ('b' <= lookahead && lookahead <= 'z')) ADVANCE(50);
+      END_STATE();
+    case 37:
+      ACCEPT_TOKEN(sym_identifier);
+      if (lookahead == 'd') ADVANCE(74);
+      if (('0' <= lookahead && lookahead <= '9') ||
+          ('A' <= lookahead && lookahead <= 'Z') ||
+          lookahead == '_' ||
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50);
+      END_STATE();
+    case 38:
+      ACCEPT_TOKEN(sym_identifier);
+      if (lookahead == 'e') ADVANCE(48);
+      if (('0' <= lookahead && lookahead <= '9') ||
+          ('A' <= lookahead && lookahead <= 'Z') ||
+          lookahead == '_' ||
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50);
+      END_STATE();
+    case 39:
+      ACCEPT_TOKEN(sym_identifier);
+      if (lookahead == 'i') ADVANCE(46);
+      if (('0' <= lookahead && lookahead <= '9') ||
+          ('A' <= lookahead && lookahead <= 'Z') ||
+          lookahead == '_' ||
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50);
+      END_STATE();
+    case 40:
+      ACCEPT_TOKEN(sym_identifier);
+      if (lookahead == 'l') ADVANCE(67);
+      if (('0' <= lookahead && lookahead <= '9') ||
+          ('A' <= lookahead && lookahead <= 'Z') ||
+          lookahead == '_' ||
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50);
+      END_STATE();
+    case 41:
+      ACCEPT_TOKEN(sym_identifier);
+      if (lookahead == 'l') ADVANCE(40);
+      if (('0' <= lookahead && lookahead <= '9') ||
+          ('A' <= lookahead && lookahead <= 'Z') ||
+          lookahead == '_' ||
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50);
+      END_STATE();
+    case 42:
+      ACCEPT_TOKEN(sym_identifier);
+      if (lookahead == 'm') ADVANCE(76);
+      if (('0' <= lookahead && lookahead <= '9') ||
+          ('A' <= lookahead && lookahead <= 'Z') ||
+          lookahead == '_' ||
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50);
+      END_STATE();
+    case 43:
+      ACCEPT_TOKEN(sym_identifier);
+      if (lookahead == 'n') ADVANCE(62);
+      if (('0' <= lookahead && lookahead <= '9') ||
+          ('A' <= lookahead && lookahead <= 'Z') ||
+          lookahead == '_' ||
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50);
+      END_STATE();
+    case 44:
+      ACCEPT_TOKEN(sym_identifier);
+      if (lookahead == 'n') ADVANCE(37);
+      if (('0' <= lookahead && lookahead <= '9') ||
+          ('A' <= lookahead && lookahead <= 'Z') ||
+          lookahead == '_' ||
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50);
+      END_STATE();
+    case 45:
+      ACCEPT_TOKEN(sym_identifier);
+      if (lookahead == 'o') ADVANCE(47);
+      if (lookahead == 'u') ADVANCE(43);
+      if (('0' <= lookahead && lookahead <= '9') ||
+          ('A' <= lookahead && lookahead <= 'Z') ||
+          lookahead == '_' ||
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50);
+      END_STATE();
+    case 46:
+      ACCEPT_TOKEN(sym_identifier);
+      if (lookahead == 'o') ADVANCE(42);
+      if (('0' <= lookahead && lookahead <= '9') ||
+          ('A' <= lookahead && lookahead <= 'Z') ||
+          lookahead == '_' ||
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50);
+      END_STATE();
+    case 47:
+      ACCEPT_TOKEN(sym_identifier);
+      if (lookahead == 'r') ADVANCE(36);
+      if (('0' <= lookahead && lookahead <= '9') ||
+          ('A' <= lookahead && lookahead <= 'Z') ||
+          lookahead == '_' ||
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50);
+      END_STATE();
+    case 48:
+      ACCEPT_TOKEN(sym_identifier);
+      if (lookahead == 't') ADVANCE(71);
+      if (('0' <= lookahead && lookahead <= '9') ||
+          ('A' <= lookahead && lookahead <= 'Z') ||
+          lookahead == '_' ||
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50);
+      END_STATE();
+    case 49:
+      ACCEPT_TOKEN(sym_identifier);
+      if (lookahead == 'x') ADVANCE(39);
+      if (('0' <= lookahead && lookahead <= '9') ||
+          ('A' <= lookahead && lookahead <= 'Z') ||
+          lookahead == '_' ||
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50);
+      END_STATE();
+    case 50:
       ACCEPT_TOKEN(sym_identifier);
       if (('0' <= lookahead && lookahead <= '9') ||
           ('A' <= lookahead && lookahead <= 'Z') ||
           lookahead == '_' ||
-          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(29);
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50);
       END_STATE();
-    case 30:
+    case 51:
       ACCEPT_TOKEN(sym_comment);
       if (lookahead != 0 &&
-          lookahead != '\n') ADVANCE(30);
+          lookahead != '\n') ADVANCE(51);
       END_STATE();
-    case 31:
+    case 52:
       ACCEPT_TOKEN(sym_block_comment);
-      if (lookahead == '\n') ADVANCE(4);
-      if (lookahead == '*') ADVANCE(52);
-      if (lookahead == '[') ADVANCE(53);
-      if (lookahead == ']') ADVANCE(57);
-      if (lookahead != 0) ADVANCE(51);
+      if (lookahead == '\n') ADVANCE(6);
+      if (lookahead == '*') ADVANCE(81);
+      if (lookahead == '[') ADVANCE(82);
+      if (lookahead == ']') ADVANCE(86);
+      if (lookahead != 0) ADVANCE(80);
       END_STATE();
-    case 32:
+    case 53:
       ACCEPT_TOKEN(sym_block_comment);
-      if (lookahead == '*') ADVANCE(8);
-      if (lookahead == '[') ADVANCE(16);
+      if (lookahead == '*') ADVANCE(10);
+      if (lookahead == '[') ADVANCE(33);
       if (lookahead != 0 &&
-          lookahead != ']') ADVANCE(4);
+          lookahead != ']') ADVANCE(6);
       END_STATE();
-    case 33:
+    case 54:
       ACCEPT_TOKEN(anon_sym_LPAREN);
       END_STATE();
-    case 34:
+    case 55:
       ACCEPT_TOKEN(anon_sym_COLON);
-      if (lookahead == '=') ADVANCE(49);
+      if (lookahead == '=') ADVANCE(69);
       END_STATE();
-    case 35:
+    case 56:
       ACCEPT_TOKEN(anon_sym_RPAREN);
       END_STATE();
-    case 36:
+    case 57:
       ACCEPT_TOKEN(sym_star);
       END_STATE();
-    case 37:
+    case 58:
       ACCEPT_TOKEN(anon_sym_u25a1);
       END_STATE();
-    case 38:
+    case 59:
       ACCEPT_TOKEN(anon_sym_LBRACK_RBRACK);
       END_STATE();
-    case 39:
+    case 60:
       ACCEPT_TOKEN(anon_sym_u03bb);
       END_STATE();
-    case 40:
+    case 61:
+      ACCEPT_TOKEN(anon_sym_fun);
+      END_STATE();
+    case 62:
       ACCEPT_TOKEN(anon_sym_fun);
       if (('0' <= lookahead && lookahead <= '9') ||
           ('A' <= lookahead && lookahead <= 'Z') ||
           lookahead == '_' ||
-          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(29);
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50);
       END_STATE();
-    case 41:
+    case 63:
       ACCEPT_TOKEN(anon_sym_EQ_GT);
       END_STATE();
-    case 42:
+    case 64:
       ACCEPT_TOKEN(anon_sym_u21d2);
       END_STATE();
-    case 43:
+    case 65:
       ACCEPT_TOKEN(anon_sym_u220f);
       END_STATE();
-    case 44:
+    case 66:
+      ACCEPT_TOKEN(anon_sym_forall);
+      END_STATE();
+    case 67:
       ACCEPT_TOKEN(anon_sym_forall);
       if (('0' <= lookahead && lookahead <= '9') ||
           ('A' <= lookahead && lookahead <= 'Z') ||
           lookahead == '_' ||
-          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(29);
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50);
       END_STATE();
-    case 45:
+    case 68:
       ACCEPT_TOKEN(anon_sym_COMMA);
       END_STATE();
-    case 46:
+    case 69:
+      ACCEPT_TOKEN(anon_sym_COLON_EQ);
+      END_STATE();
+    case 70:
+      ACCEPT_TOKEN(anon_sym_let);
+      END_STATE();
+    case 71:
+      ACCEPT_TOKEN(anon_sym_let);
+      if (('0' <= lookahead && lookahead <= '9') ||
+          ('A' <= lookahead && lookahead <= 'Z') ||
+          lookahead == '_' ||
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50);
+      END_STATE();
+    case 72:
+      ACCEPT_TOKEN(anon_sym_in);
+      END_STATE();
+    case 73:
+      ACCEPT_TOKEN(anon_sym_end);
+      END_STATE();
+    case 74:
+      ACCEPT_TOKEN(anon_sym_end);
+      if (('0' <= lookahead && lookahead <= '9') ||
+          ('A' <= lookahead && lookahead <= 'Z') ||
+          lookahead == '_' ||
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50);
+      END_STATE();
+    case 75:
+      ACCEPT_TOKEN(sym_axiom);
+      END_STATE();
+    case 76:
       ACCEPT_TOKEN(sym_axiom);
       if (('0' <= lookahead && lookahead <= '9') ||
           ('A' <= lookahead && lookahead <= 'Z') ||
           lookahead == '_' ||
-          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(29);
+          ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50);
       END_STATE();
-    case 47:
+    case 77:
       ACCEPT_TOKEN(anon_sym_DASH_GT);
       END_STATE();
-    case 48:
+    case 78:
       ACCEPT_TOKEN(anon_sym_u2192);
       END_STATE();
-    case 49:
-      ACCEPT_TOKEN(anon_sym_COLON_EQ);
-      END_STATE();
-    case 50:
+    case 79:
       ACCEPT_TOKEN(anon_sym_SEMI);
       END_STATE();
-    case 51:
+    case 80:
       ACCEPT_TOKEN(sym_post_command);
-      if (lookahead == '\n') ADVANCE(4);
-      if (lookahead == '*') ADVANCE(52);
-      if (lookahead == '[') ADVANCE(53);
-      if (lookahead == ']') ADVANCE(57);
-      if (lookahead != 0) ADVANCE(51);
+      if (lookahead == '\n') ADVANCE(6);
+      if (lookahead == '*') ADVANCE(81);
+      if (lookahead == '[') ADVANCE(82);
+      if (lookahead == ']') ADVANCE(86);
+      if (lookahead != 0) ADVANCE(80);
       END_STATE();
-    case 52:
+    case 81:
       ACCEPT_TOKEN(sym_post_command);
-      if (lookahead == '\n') ADVANCE(4);
-      if (lookahead == ']') ADVANCE(31);
-      if (lookahead != 0) ADVANCE(51);
+      if (lookahead == '\n') ADVANCE(6);
+      if (lookahead == ']') ADVANCE(52);
+      if (lookahead != 0) ADVANCE(80);
       END_STATE();
-    case 53:
+    case 82:
       ACCEPT_TOKEN(sym_post_command);
-      if (lookahead == '\n') ADVANCE(4);
-      if (lookahead != 0) ADVANCE(51);
+      if (lookahead == '\n') ADVANCE(6);
+      if (lookahead != 0) ADVANCE(80);
       END_STATE();
-    case 54:
+    case 83:
       ACCEPT_TOKEN(sym_post_command);
-      if (lookahead == '*') ADVANCE(51);
+      if (lookahead == '*') ADVANCE(80);
       if (lookahead != 0 &&
-          lookahead != '\n') ADVANCE(57);
+          lookahead != '\n') ADVANCE(86);
       END_STATE();
-    case 55:
+    case 84:
       ACCEPT_TOKEN(sym_post_command);
-      if (lookahead == '-') ADVANCE(30);
+      if (lookahead == '-') ADVANCE(51);
       if (lookahead != 0 &&
-          lookahead != '\n') ADVANCE(57);
+          lookahead != '\n') ADVANCE(86);
       END_STATE();
-    case 56:
+    case 85:
       ACCEPT_TOKEN(sym_post_command);
-      if (lookahead == '-') ADVANCE(55);
-      if (lookahead == '[') ADVANCE(54);
+      if (lookahead == '-') ADVANCE(84);
+      if (lookahead == '[') ADVANCE(83);
       if (lookahead == '\t' ||
           (0x0b <= lookahead && lookahead <= '\r') ||
-          lookahead == ' ') ADVANCE(56);
+          lookahead == ' ') ADVANCE(85);
       if (lookahead != 0 &&
-          (lookahead < '\t' || '\r' < lookahead)) ADVANCE(57);
+          (lookahead < '\t' || '\r' < lookahead)) ADVANCE(86);
       END_STATE();
-    case 57:
+    case 86:
       ACCEPT_TOKEN(sym_post_command);
       if (lookahead != 0 &&
-          lookahead != '\n') ADVANCE(57);
+          lookahead != '\n') ADVANCE(86);
       END_STATE();
-    case 58:
+    case 87:
       ACCEPT_TOKEN(sym_command);
       END_STATE();
     default:
@@ -766,63 +978,88 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) {
 
 static const TSLexMode ts_lex_modes[STATE_COUNT] = {
   [0] = {.lex_state = 0},
-  [1] = {.lex_state = 17},
-  [2] = {.lex_state = 0},
-  [3] = {.lex_state = 0},
-  [4] = {.lex_state = 0},
-  [5] = {.lex_state = 2},
-  [6] = {.lex_state = 2},
-  [7] = {.lex_state = 2},
-  [8] = {.lex_state = 2},
-  [9] = {.lex_state = 2},
-  [10] = {.lex_state = 2},
-  [11] = {.lex_state = 2},
-  [12] = {.lex_state = 17},
-  [13] = {.lex_state = 17},
-  [14] = {.lex_state = 17},
-  [15] = {.lex_state = 17},
-  [16] = {.lex_state = 17},
-  [17] = {.lex_state = 0},
-  [18] = {.lex_state = 17},
-  [19] = {.lex_state = 0},
-  [20] = {.lex_state = 0},
-  [21] = {.lex_state = 0},
-  [22] = {.lex_state = 17},
-  [23] = {.lex_state = 0},
-  [24] = {.lex_state = 0},
+  [1] = {.lex_state = 34},
+  [2] = {.lex_state = 3},
+  [3] = {.lex_state = 3},
+  [4] = {.lex_state = 3},
+  [5] = {.lex_state = 4},
+  [6] = {.lex_state = 4},
+  [7] = {.lex_state = 4},
+  [8] = {.lex_state = 4},
+  [9] = {.lex_state = 4},
+  [10] = {.lex_state = 4},
+  [11] = {.lex_state = 4},
+  [12] = {.lex_state = 4},
+  [13] = {.lex_state = 4},
+  [14] = {.lex_state = 4},
+  [15] = {.lex_state = 4},
+  [16] = {.lex_state = 4},
+  [17] = {.lex_state = 4},
+  [18] = {.lex_state = 34},
+  [19] = {.lex_state = 34},
+  [20] = {.lex_state = 2},
+  [21] = {.lex_state = 2},
+  [22] = {.lex_state = 34},
+  [23] = {.lex_state = 34},
+  [24] = {.lex_state = 34},
   [25] = {.lex_state = 0},
-  [26] = {.lex_state = 0},
-  [27] = {.lex_state = 0},
-  [28] = {.lex_state = 0},
-  [29] = {.lex_state = 0},
+  [26] = {.lex_state = 2},
+  [27] = {.lex_state = 2},
+  [28] = {.lex_state = 2},
+  [29] = {.lex_state = 34},
   [30] = {.lex_state = 0},
   [31] = {.lex_state = 0},
-  [32] = {.lex_state = 17},
+  [32] = {.lex_state = 0},
   [33] = {.lex_state = 0},
-  [34] = {.lex_state = 17},
+  [34] = {.lex_state = 0},
   [35] = {.lex_state = 0},
-  [36] = {.lex_state = 17},
-  [37] = {.lex_state = 17},
-  [38] = {.lex_state = 17},
-  [39] = {.lex_state = 17},
-  [40] = {.lex_state = 17},
+  [36] = {.lex_state = 0},
+  [37] = {.lex_state = 34},
+  [38] = {.lex_state = 0},
+  [39] = {.lex_state = 0},
+  [40] = {.lex_state = 0},
   [41] = {.lex_state = 0},
   [42] = {.lex_state = 0},
   [43] = {.lex_state = 0},
   [44] = {.lex_state = 0},
   [45] = {.lex_state = 0},
-  [46] = {.lex_state = 1},
+  [46] = {.lex_state = 0},
   [47] = {.lex_state = 0},
   [48] = {.lex_state = 0},
-  [49] = {.lex_state = 0},
-  [50] = {.lex_state = 0},
-  [51] = {.lex_state = 0},
+  [49] = {.lex_state = 34},
+  [50] = {.lex_state = 34},
+  [51] = {.lex_state = 34},
+  [52] = {.lex_state = 34},
+  [53] = {.lex_state = 34},
+  [54] = {.lex_state = 0},
+  [55] = {.lex_state = 34},
+  [56] = {.lex_state = 34},
+  [57] = {.lex_state = 0},
+  [58] = {.lex_state = 0},
+  [59] = {.lex_state = 0},
+  [60] = {.lex_state = 0},
+  [61] = {.lex_state = 0},
+  [62] = {.lex_state = 0},
+  [63] = {.lex_state = 0},
+  [64] = {.lex_state = 34},
+  [65] = {.lex_state = 0},
+  [66] = {.lex_state = 0},
+  [67] = {.lex_state = 0},
+  [68] = {.lex_state = 0},
+  [69] = {.lex_state = 0},
+  [70] = {.lex_state = 0},
+  [71] = {.lex_state = 0},
+  [72] = {.lex_state = 1},
+  [73] = {.lex_state = 0},
+  [74] = {.lex_state = 0},
+  [75] = {.lex_state = 0},
+  [76] = {.lex_state = 0},
+  [77] = {.lex_state = 0},
 };
 
 static const uint16_t ts_parse_table[LARGE_STATE_COUNT][SYMBOL_COUNT] = {
   [0] = {
     [ts_builtin_sym_end] = ACTIONS(1),
-    [sym_identifier] = ACTIONS(1),
     [sym_comment] = ACTIONS(3),
     [sym_block_comment] = ACTIONS(3),
     [anon_sym_LPAREN] = ACTIONS(1),
@@ -838,97 +1075,31 @@ static const uint16_t ts_parse_table[LARGE_STATE_COUNT][SYMBOL_COUNT] = {
     [anon_sym_u220f] = ACTIONS(1),
     [anon_sym_forall] = ACTIONS(1),
     [anon_sym_COMMA] = ACTIONS(1),
+    [anon_sym_COLON_EQ] = ACTIONS(1),
+    [anon_sym_let] = ACTIONS(1),
+    [anon_sym_in] = ACTIONS(1),
+    [anon_sym_end] = ACTIONS(1),
     [sym_axiom] = ACTIONS(1),
     [anon_sym_DASH_GT] = ACTIONS(1),
     [anon_sym_u2192] = ACTIONS(1),
-    [anon_sym_COLON_EQ] = ACTIONS(1),
     [anon_sym_SEMI] = ACTIONS(1),
     [sym_command] = ACTIONS(1),
   },
   [1] = {
-    [sym_program] = STATE(45),
-    [sym_definition] = STATE(18),
-    [sym_preprocess] = STATE(18),
-    [aux_sym_program_repeat1] = STATE(18),
+    [sym_program] = STATE(75),
+    [sym_definition] = STATE(37),
+    [sym_preprocess] = STATE(37),
+    [aux_sym_program_repeat1] = STATE(37),
     [ts_builtin_sym_end] = ACTIONS(5),
     [sym_identifier] = ACTIONS(7),
     [sym_comment] = ACTIONS(3),
     [sym_block_comment] = ACTIONS(3),
     [sym_command] = ACTIONS(9),
   },
-  [2] = {
-    [sym_square] = STATE(14),
-    [sym_labs] = STATE(26),
-    [sym_pabs] = STATE(26),
-    [sym_term] = STATE(12),
-    [sym_app] = STATE(26),
-    [sym_arrow] = STATE(25),
-    [sym_app_term] = STATE(24),
-    [sym_expr] = STATE(43),
-    [aux_sym_app_repeat1] = STATE(12),
-    [sym_identifier] = ACTIONS(11),
-    [sym_comment] = ACTIONS(3),
-    [sym_block_comment] = ACTIONS(3),
-    [anon_sym_LPAREN] = ACTIONS(13),
-    [sym_star] = ACTIONS(15),
-    [anon_sym_u25a1] = ACTIONS(17),
-    [anon_sym_LBRACK_RBRACK] = ACTIONS(17),
-    [anon_sym_u03bb] = ACTIONS(19),
-    [anon_sym_fun] = ACTIONS(21),
-    [anon_sym_u220f] = ACTIONS(23),
-    [anon_sym_forall] = ACTIONS(25),
-    [sym_axiom] = ACTIONS(27),
-  },
-  [3] = {
-    [sym_square] = STATE(14),
-    [sym_labs] = STATE(26),
-    [sym_pabs] = STATE(26),
-    [sym_term] = STATE(12),
-    [sym_app] = STATE(26),
-    [sym_arrow] = STATE(25),
-    [sym_app_term] = STATE(24),
-    [sym_expr] = STATE(48),
-    [aux_sym_app_repeat1] = STATE(12),
-    [sym_identifier] = ACTIONS(11),
-    [sym_comment] = ACTIONS(3),
-    [sym_block_comment] = ACTIONS(3),
-    [anon_sym_LPAREN] = ACTIONS(13),
-    [sym_star] = ACTIONS(15),
-    [anon_sym_u25a1] = ACTIONS(17),
-    [anon_sym_LBRACK_RBRACK] = ACTIONS(17),
-    [anon_sym_u03bb] = ACTIONS(19),
-    [anon_sym_fun] = ACTIONS(21),
-    [anon_sym_u220f] = ACTIONS(23),
-    [anon_sym_forall] = ACTIONS(25),
-    [sym_axiom] = ACTIONS(29),
-  },
-  [4] = {
-    [sym_square] = STATE(14),
-    [sym_labs] = STATE(26),
-    [sym_pabs] = STATE(26),
-    [sym_term] = STATE(12),
-    [sym_app] = STATE(26),
-    [sym_arrow] = STATE(25),
-    [sym_app_term] = STATE(24),
-    [sym_expr] = STATE(47),
-    [aux_sym_app_repeat1] = STATE(12),
-    [sym_identifier] = ACTIONS(11),
-    [sym_comment] = ACTIONS(3),
-    [sym_block_comment] = ACTIONS(3),
-    [anon_sym_LPAREN] = ACTIONS(13),
-    [sym_star] = ACTIONS(15),
-    [anon_sym_u25a1] = ACTIONS(17),
-    [anon_sym_LBRACK_RBRACK] = ACTIONS(17),
-    [anon_sym_u03bb] = ACTIONS(19),
-    [anon_sym_fun] = ACTIONS(21),
-    [anon_sym_u220f] = ACTIONS(23),
-    [anon_sym_forall] = ACTIONS(25),
-    [sym_axiom] = ACTIONS(31),
-  },
 };
 
 static const uint16_t ts_small_parse_table[] = {
-  [0] = 15,
+  [0] = 17,
     ACTIONS(11), 1,
       sym_identifier,
     ACTIONS(13), 1,
@@ -943,157 +1114,17 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_u220f,
     ACTIONS(25), 1,
       anon_sym_forall,
-    STATE(14), 1,
-      sym_square,
+    ACTIONS(27), 1,
+      anon_sym_let,
+    ACTIONS(29), 1,
+      sym_axiom,
     STATE(24), 1,
-      sym_app_term,
-    STATE(25), 1,
-      sym_arrow,
-    STATE(49), 1,
-      sym_expr,
-    ACTIONS(3), 2,
-      sym_comment,
-      sym_block_comment,
-    ACTIONS(17), 2,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-    STATE(12), 2,
-      sym_term,
-      aux_sym_app_repeat1,
-    STATE(26), 3,
-      sym_labs,
-      sym_pabs,
-      sym_app,
-  [51] = 15,
-    ACTIONS(11), 1,
-      sym_identifier,
-    ACTIONS(13), 1,
-      anon_sym_LPAREN,
-    ACTIONS(15), 1,
-      sym_star,
-    ACTIONS(19), 1,
-      anon_sym_u03bb,
-    ACTIONS(21), 1,
-      anon_sym_fun,
-    ACTIONS(23), 1,
-      anon_sym_u220f,
-    ACTIONS(25), 1,
-      anon_sym_forall,
-    STATE(14), 1,
       sym_square,
-    STATE(24), 1,
-      sym_app_term,
-    STATE(25), 1,
-      sym_arrow,
-    STATE(50), 1,
-      sym_expr,
-    ACTIONS(3), 2,
-      sym_comment,
-      sym_block_comment,
-    ACTIONS(17), 2,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-    STATE(12), 2,
-      sym_term,
-      aux_sym_app_repeat1,
-    STATE(26), 3,
-      sym_labs,
-      sym_pabs,
-      sym_app,
-  [102] = 15,
-    ACTIONS(11), 1,
-      sym_identifier,
-    ACTIONS(13), 1,
-      anon_sym_LPAREN,
-    ACTIONS(15), 1,
-      sym_star,
-    ACTIONS(19), 1,
-      anon_sym_u03bb,
-    ACTIONS(21), 1,
-      anon_sym_fun,
-    ACTIONS(23), 1,
-      anon_sym_u220f,
-    ACTIONS(25), 1,
-      anon_sym_forall,
-    STATE(14), 1,
-      sym_square,
-    STATE(24), 1,
-      sym_app_term,
-    STATE(25), 1,
-      sym_arrow,
-    STATE(41), 1,
-      sym_expr,
-    ACTIONS(3), 2,
-      sym_comment,
-      sym_block_comment,
-    ACTIONS(17), 2,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-    STATE(12), 2,
-      sym_term,
-      aux_sym_app_repeat1,
-    STATE(26), 3,
-      sym_labs,
-      sym_pabs,
-      sym_app,
-  [153] = 15,
-    ACTIONS(11), 1,
-      sym_identifier,
-    ACTIONS(13), 1,
-      anon_sym_LPAREN,
-    ACTIONS(15), 1,
-      sym_star,
-    ACTIONS(19), 1,
-      anon_sym_u03bb,
-    ACTIONS(21), 1,
-      anon_sym_fun,
-    ACTIONS(23), 1,
-      anon_sym_u220f,
-    ACTIONS(25), 1,
-      anon_sym_forall,
-    STATE(14), 1,
-      sym_square,
-    STATE(24), 1,
-      sym_app_term,
-    STATE(25), 1,
-      sym_arrow,
-    STATE(51), 1,
-      sym_expr,
-    ACTIONS(3), 2,
-      sym_comment,
-      sym_block_comment,
-    ACTIONS(17), 2,
-      anon_sym_u25a1,
-      anon_sym_LBRACK_RBRACK,
-    STATE(12), 2,
-      sym_term,
-      aux_sym_app_repeat1,
-    STATE(26), 3,
-      sym_labs,
-      sym_pabs,
-      sym_app,
-  [204] = 15,
-    ACTIONS(11), 1,
-      sym_identifier,
-    ACTIONS(13), 1,
-      anon_sym_LPAREN,
-    ACTIONS(15), 1,
-      sym_star,
-    ACTIONS(19), 1,
-      anon_sym_u03bb,
-    ACTIONS(21), 1,
-      anon_sym_fun,
-    ACTIONS(23), 1,
-      anon_sym_u220f,
-    ACTIONS(25), 1,
-      anon_sym_forall,
-    STATE(14), 1,
-      sym_square,
-    STATE(24), 1,
-      sym_app_term,
-    STATE(25), 1,
-      sym_arrow,
     STATE(30), 1,
+      sym_arrow,
+    STATE(42), 1,
+      sym_app_term,
+    STATE(71), 1,
       sym_expr,
     ACTIONS(3), 2,
       sym_comment,
@@ -1101,14 +1132,15 @@ static const uint16_t ts_small_parse_table[] = {
     ACTIONS(17), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(12), 2,
+    STATE(18), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(26), 3,
+    STATE(40), 4,
       sym_labs,
       sym_pabs,
+      sym_let,
       sym_app,
-  [255] = 15,
+  [58] = 17,
     ACTIONS(11), 1,
       sym_identifier,
     ACTIONS(13), 1,
@@ -1123,13 +1155,17 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_u220f,
     ACTIONS(25), 1,
       anon_sym_forall,
-    STATE(14), 1,
-      sym_square,
+    ACTIONS(27), 1,
+      anon_sym_let,
+    ACTIONS(31), 1,
+      sym_axiom,
     STATE(24), 1,
-      sym_app_term,
-    STATE(25), 1,
+      sym_square,
+    STATE(30), 1,
       sym_arrow,
-    STATE(28), 1,
+    STATE(42), 1,
+      sym_app_term,
+    STATE(66), 1,
       sym_expr,
     ACTIONS(3), 2,
       sym_comment,
@@ -1137,14 +1173,15 @@ static const uint16_t ts_small_parse_table[] = {
     ACTIONS(17), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(12), 2,
+    STATE(18), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(26), 3,
+    STATE(40), 4,
       sym_labs,
       sym_pabs,
+      sym_let,
       sym_app,
-  [306] = 15,
+  [116] = 17,
     ACTIONS(11), 1,
       sym_identifier,
     ACTIONS(13), 1,
@@ -1159,13 +1196,17 @@ static const uint16_t ts_small_parse_table[] = {
       anon_sym_u220f,
     ACTIONS(25), 1,
       anon_sym_forall,
-    STATE(14), 1,
-      sym_square,
+    ACTIONS(27), 1,
+      anon_sym_let,
+    ACTIONS(33), 1,
+      sym_axiom,
     STATE(24), 1,
-      sym_app_term,
-    STATE(25), 1,
+      sym_square,
+    STATE(30), 1,
       sym_arrow,
-    STATE(29), 1,
+    STATE(42), 1,
+      sym_app_term,
+    STATE(62), 1,
       sym_expr,
     ACTIONS(3), 2,
       sym_comment,
@@ -1173,17 +1214,525 @@ static const uint16_t ts_small_parse_table[] = {
     ACTIONS(17), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(12), 2,
+    STATE(18), 2,
       sym_term,
       aux_sym_app_repeat1,
-    STATE(26), 3,
+    STATE(40), 4,
       sym_labs,
       sym_pabs,
+      sym_let,
       sym_app,
-  [357] = 7,
+  [174] = 16,
+    ACTIONS(11), 1,
+      sym_identifier,
     ACTIONS(13), 1,
       anon_sym_LPAREN,
-    STATE(14), 1,
+    ACTIONS(15), 1,
+      sym_star,
+    ACTIONS(19), 1,
+      anon_sym_u03bb,
+    ACTIONS(21), 1,
+      anon_sym_fun,
+    ACTIONS(23), 1,
+      anon_sym_u220f,
+    ACTIONS(25), 1,
+      anon_sym_forall,
+    ACTIONS(27), 1,
+      anon_sym_let,
+    STATE(24), 1,
+      sym_square,
+    STATE(30), 1,
+      sym_arrow,
+    STATE(42), 1,
+      sym_app_term,
+    STATE(76), 1,
+      sym_expr,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    ACTIONS(17), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(18), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+    STATE(40), 4,
+      sym_labs,
+      sym_pabs,
+      sym_let,
+      sym_app,
+  [229] = 16,
+    ACTIONS(11), 1,
+      sym_identifier,
+    ACTIONS(13), 1,
+      anon_sym_LPAREN,
+    ACTIONS(15), 1,
+      sym_star,
+    ACTIONS(19), 1,
+      anon_sym_u03bb,
+    ACTIONS(21), 1,
+      anon_sym_fun,
+    ACTIONS(23), 1,
+      anon_sym_u220f,
+    ACTIONS(25), 1,
+      anon_sym_forall,
+    ACTIONS(27), 1,
+      anon_sym_let,
+    STATE(24), 1,
+      sym_square,
+    STATE(30), 1,
+      sym_arrow,
+    STATE(42), 1,
+      sym_app_term,
+    STATE(63), 1,
+      sym_expr,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    ACTIONS(17), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(18), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+    STATE(40), 4,
+      sym_labs,
+      sym_pabs,
+      sym_let,
+      sym_app,
+  [284] = 16,
+    ACTIONS(11), 1,
+      sym_identifier,
+    ACTIONS(13), 1,
+      anon_sym_LPAREN,
+    ACTIONS(15), 1,
+      sym_star,
+    ACTIONS(19), 1,
+      anon_sym_u03bb,
+    ACTIONS(21), 1,
+      anon_sym_fun,
+    ACTIONS(23), 1,
+      anon_sym_u220f,
+    ACTIONS(25), 1,
+      anon_sym_forall,
+    ACTIONS(27), 1,
+      anon_sym_let,
+    STATE(24), 1,
+      sym_square,
+    STATE(30), 1,
+      sym_arrow,
+    STATE(42), 1,
+      sym_app_term,
+    STATE(68), 1,
+      sym_expr,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    ACTIONS(17), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(18), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+    STATE(40), 4,
+      sym_labs,
+      sym_pabs,
+      sym_let,
+      sym_app,
+  [339] = 16,
+    ACTIONS(11), 1,
+      sym_identifier,
+    ACTIONS(13), 1,
+      anon_sym_LPAREN,
+    ACTIONS(15), 1,
+      sym_star,
+    ACTIONS(19), 1,
+      anon_sym_u03bb,
+    ACTIONS(21), 1,
+      anon_sym_fun,
+    ACTIONS(23), 1,
+      anon_sym_u220f,
+    ACTIONS(25), 1,
+      anon_sym_forall,
+    ACTIONS(27), 1,
+      anon_sym_let,
+    STATE(24), 1,
+      sym_square,
+    STATE(30), 1,
+      sym_arrow,
+    STATE(33), 1,
+      sym_expr,
+    STATE(42), 1,
+      sym_app_term,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    ACTIONS(17), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(18), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+    STATE(40), 4,
+      sym_labs,
+      sym_pabs,
+      sym_let,
+      sym_app,
+  [394] = 16,
+    ACTIONS(11), 1,
+      sym_identifier,
+    ACTIONS(13), 1,
+      anon_sym_LPAREN,
+    ACTIONS(15), 1,
+      sym_star,
+    ACTIONS(19), 1,
+      anon_sym_u03bb,
+    ACTIONS(21), 1,
+      anon_sym_fun,
+    ACTIONS(23), 1,
+      anon_sym_u220f,
+    ACTIONS(25), 1,
+      anon_sym_forall,
+    ACTIONS(27), 1,
+      anon_sym_let,
+    STATE(24), 1,
+      sym_square,
+    STATE(30), 1,
+      sym_arrow,
+    STATE(42), 1,
+      sym_app_term,
+    STATE(73), 1,
+      sym_expr,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    ACTIONS(17), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(18), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+    STATE(40), 4,
+      sym_labs,
+      sym_pabs,
+      sym_let,
+      sym_app,
+  [449] = 16,
+    ACTIONS(11), 1,
+      sym_identifier,
+    ACTIONS(13), 1,
+      anon_sym_LPAREN,
+    ACTIONS(15), 1,
+      sym_star,
+    ACTIONS(19), 1,
+      anon_sym_u03bb,
+    ACTIONS(21), 1,
+      anon_sym_fun,
+    ACTIONS(23), 1,
+      anon_sym_u220f,
+    ACTIONS(25), 1,
+      anon_sym_forall,
+    ACTIONS(27), 1,
+      anon_sym_let,
+    STATE(24), 1,
+      sym_square,
+    STATE(30), 1,
+      sym_arrow,
+    STATE(38), 1,
+      sym_expr,
+    STATE(42), 1,
+      sym_app_term,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    ACTIONS(17), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(18), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+    STATE(40), 4,
+      sym_labs,
+      sym_pabs,
+      sym_let,
+      sym_app,
+  [504] = 16,
+    ACTIONS(27), 1,
+      anon_sym_let,
+    ACTIONS(35), 1,
+      sym_identifier,
+    ACTIONS(37), 1,
+      anon_sym_LPAREN,
+    ACTIONS(39), 1,
+      sym_star,
+    ACTIONS(43), 1,
+      anon_sym_u03bb,
+    ACTIONS(45), 1,
+      anon_sym_fun,
+    ACTIONS(47), 1,
+      anon_sym_u220f,
+    ACTIONS(49), 1,
+      anon_sym_forall,
+    STATE(26), 1,
+      sym_square,
+    STATE(30), 1,
+      sym_arrow,
+    STATE(57), 1,
+      sym_app_term,
+    STATE(67), 1,
+      sym_expr,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    ACTIONS(41), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(21), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+    STATE(40), 4,
+      sym_labs,
+      sym_pabs,
+      sym_let,
+      sym_app,
+  [559] = 16,
+    ACTIONS(11), 1,
+      sym_identifier,
+    ACTIONS(13), 1,
+      anon_sym_LPAREN,
+    ACTIONS(15), 1,
+      sym_star,
+    ACTIONS(19), 1,
+      anon_sym_u03bb,
+    ACTIONS(21), 1,
+      anon_sym_fun,
+    ACTIONS(23), 1,
+      anon_sym_u220f,
+    ACTIONS(25), 1,
+      anon_sym_forall,
+    ACTIONS(27), 1,
+      anon_sym_let,
+    STATE(24), 1,
+      sym_square,
+    STATE(30), 1,
+      sym_arrow,
+    STATE(39), 1,
+      sym_expr,
+    STATE(42), 1,
+      sym_app_term,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    ACTIONS(17), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(18), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+    STATE(40), 4,
+      sym_labs,
+      sym_pabs,
+      sym_let,
+      sym_app,
+  [614] = 16,
+    ACTIONS(11), 1,
+      sym_identifier,
+    ACTIONS(13), 1,
+      anon_sym_LPAREN,
+    ACTIONS(15), 1,
+      sym_star,
+    ACTIONS(19), 1,
+      anon_sym_u03bb,
+    ACTIONS(21), 1,
+      anon_sym_fun,
+    ACTIONS(23), 1,
+      anon_sym_u220f,
+    ACTIONS(25), 1,
+      anon_sym_forall,
+    ACTIONS(27), 1,
+      anon_sym_let,
+    STATE(24), 1,
+      sym_square,
+    STATE(30), 1,
+      sym_arrow,
+    STATE(42), 1,
+      sym_app_term,
+    STATE(70), 1,
+      sym_expr,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    ACTIONS(17), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(18), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+    STATE(40), 4,
+      sym_labs,
+      sym_pabs,
+      sym_let,
+      sym_app,
+  [669] = 16,
+    ACTIONS(27), 1,
+      anon_sym_let,
+    ACTIONS(35), 1,
+      sym_identifier,
+    ACTIONS(37), 1,
+      anon_sym_LPAREN,
+    ACTIONS(39), 1,
+      sym_star,
+    ACTIONS(43), 1,
+      anon_sym_u03bb,
+    ACTIONS(45), 1,
+      anon_sym_fun,
+    ACTIONS(47), 1,
+      anon_sym_u220f,
+    ACTIONS(49), 1,
+      anon_sym_forall,
+    STATE(26), 1,
+      sym_square,
+    STATE(30), 1,
+      sym_arrow,
+    STATE(33), 1,
+      sym_expr,
+    STATE(57), 1,
+      sym_app_term,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    ACTIONS(41), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(21), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+    STATE(40), 4,
+      sym_labs,
+      sym_pabs,
+      sym_let,
+      sym_app,
+  [724] = 16,
+    ACTIONS(27), 1,
+      anon_sym_let,
+    ACTIONS(35), 1,
+      sym_identifier,
+    ACTIONS(37), 1,
+      anon_sym_LPAREN,
+    ACTIONS(39), 1,
+      sym_star,
+    ACTIONS(43), 1,
+      anon_sym_u03bb,
+    ACTIONS(45), 1,
+      anon_sym_fun,
+    ACTIONS(47), 1,
+      anon_sym_u220f,
+    ACTIONS(49), 1,
+      anon_sym_forall,
+    STATE(26), 1,
+      sym_square,
+    STATE(30), 1,
+      sym_arrow,
+    STATE(39), 1,
+      sym_expr,
+    STATE(57), 1,
+      sym_app_term,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    ACTIONS(41), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(21), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+    STATE(40), 4,
+      sym_labs,
+      sym_pabs,
+      sym_let,
+      sym_app,
+  [779] = 16,
+    ACTIONS(27), 1,
+      anon_sym_let,
+    ACTIONS(35), 1,
+      sym_identifier,
+    ACTIONS(37), 1,
+      anon_sym_LPAREN,
+    ACTIONS(39), 1,
+      sym_star,
+    ACTIONS(43), 1,
+      anon_sym_u03bb,
+    ACTIONS(45), 1,
+      anon_sym_fun,
+    ACTIONS(47), 1,
+      anon_sym_u220f,
+    ACTIONS(49), 1,
+      anon_sym_forall,
+    STATE(26), 1,
+      sym_square,
+    STATE(30), 1,
+      sym_arrow,
+    STATE(38), 1,
+      sym_expr,
+    STATE(57), 1,
+      sym_app_term,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    ACTIONS(41), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(21), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+    STATE(40), 4,
+      sym_labs,
+      sym_pabs,
+      sym_let,
+      sym_app,
+  [834] = 16,
+    ACTIONS(11), 1,
+      sym_identifier,
+    ACTIONS(13), 1,
+      anon_sym_LPAREN,
+    ACTIONS(15), 1,
+      sym_star,
+    ACTIONS(19), 1,
+      anon_sym_u03bb,
+    ACTIONS(21), 1,
+      anon_sym_fun,
+    ACTIONS(23), 1,
+      anon_sym_u220f,
+    ACTIONS(25), 1,
+      anon_sym_forall,
+    ACTIONS(27), 1,
+      anon_sym_let,
+    STATE(24), 1,
+      sym_square,
+    STATE(30), 1,
+      sym_arrow,
+    STATE(42), 1,
+      sym_app_term,
+    STATE(74), 1,
+      sym_expr,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    ACTIONS(17), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(18), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+    STATE(40), 4,
+      sym_labs,
+      sym_pabs,
+      sym_let,
+      sym_app,
+  [889] = 7,
+    ACTIONS(13), 1,
+      anon_sym_LPAREN,
+    STATE(24), 1,
       sym_square,
     ACTIONS(3), 2,
       sym_comment,
@@ -1194,461 +1743,712 @@ static const uint16_t ts_small_parse_table[] = {
     ACTIONS(17), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(13), 2,
+    STATE(19), 2,
       sym_term,
       aux_sym_app_repeat1,
-    ACTIONS(33), 5,
+    ACTIONS(51), 5,
       anon_sym_RPAREN,
+      anon_sym_COLON_EQ,
       anon_sym_DASH_GT,
       anon_sym_u2192,
-      anon_sym_COLON_EQ,
       anon_sym_SEMI,
-  [387] = 7,
-    ACTIONS(38), 1,
+  [919] = 7,
+    ACTIONS(56), 1,
       anon_sym_LPAREN,
-    STATE(14), 1,
+    STATE(24), 1,
       sym_square,
     ACTIONS(3), 2,
       sym_comment,
       sym_block_comment,
-    ACTIONS(35), 2,
+    ACTIONS(53), 2,
       sym_identifier,
       sym_star,
-    ACTIONS(43), 2,
+    ACTIONS(61), 2,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
-    STATE(13), 2,
+    STATE(19), 2,
       sym_term,
       aux_sym_app_repeat1,
-    ACTIONS(41), 5,
+    ACTIONS(59), 5,
       anon_sym_RPAREN,
+      anon_sym_COLON_EQ,
       anon_sym_DASH_GT,
       anon_sym_u2192,
-      anon_sym_COLON_EQ,
       anon_sym_SEMI,
-  [417] = 2,
+  [949] = 9,
+    ACTIONS(64), 1,
+      sym_identifier,
+    ACTIONS(67), 1,
+      anon_sym_LPAREN,
+    ACTIONS(70), 1,
+      sym_star,
+    ACTIONS(76), 1,
+      anon_sym_end,
+    STATE(26), 1,
+      sym_square,
     ACTIONS(3), 2,
       sym_comment,
       sym_block_comment,
-    ACTIONS(46), 10,
+    ACTIONS(59), 2,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+    ACTIONS(73), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    STATE(20), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+  [981] = 9,
+    ACTIONS(35), 1,
+      sym_identifier,
+    ACTIONS(37), 1,
+      anon_sym_LPAREN,
+    ACTIONS(39), 1,
+      sym_star,
+    ACTIONS(78), 1,
+      anon_sym_end,
+    STATE(26), 1,
+      sym_square,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    ACTIONS(41), 2,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+    ACTIONS(51), 2,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+    STATE(20), 2,
+      sym_term,
+      aux_sym_app_repeat1,
+  [1013] = 2,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    ACTIONS(80), 10,
       sym_identifier,
       anon_sym_LPAREN,
       anon_sym_RPAREN,
       sym_star,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
+      anon_sym_COLON_EQ,
       anon_sym_DASH_GT,
       anon_sym_u2192,
-      anon_sym_COLON_EQ,
       anon_sym_SEMI,
-  [434] = 2,
+  [1030] = 2,
     ACTIONS(3), 2,
       sym_comment,
       sym_block_comment,
-    ACTIONS(48), 10,
+    ACTIONS(82), 10,
       sym_identifier,
       anon_sym_LPAREN,
       anon_sym_RPAREN,
       sym_star,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
+      anon_sym_COLON_EQ,
       anon_sym_DASH_GT,
       anon_sym_u2192,
-      anon_sym_COLON_EQ,
       anon_sym_SEMI,
-  [451] = 2,
+  [1047] = 2,
     ACTIONS(3), 2,
       sym_comment,
       sym_block_comment,
-    ACTIONS(50), 10,
+    ACTIONS(84), 10,
       sym_identifier,
       anon_sym_LPAREN,
       anon_sym_RPAREN,
       sym_star,
       anon_sym_u25a1,
       anon_sym_LBRACK_RBRACK,
+      anon_sym_COLON_EQ,
       anon_sym_DASH_GT,
       anon_sym_u2192,
-      anon_sym_COLON_EQ,
       anon_sym_SEMI,
-  [468] = 5,
-    ACTIONS(52), 1,
+  [1064] = 5,
+    ACTIONS(86), 1,
       anon_sym_LPAREN,
-    ACTIONS(55), 1,
+    ACTIONS(89), 1,
       anon_sym_COLON,
     ACTIONS(3), 2,
       sym_comment,
       sym_block_comment,
-    STATE(17), 2,
+    STATE(25), 2,
       sym_param_block,
       aux_sym_labs_repeat1,
-    ACTIONS(57), 4,
+    ACTIONS(91), 4,
       anon_sym_EQ_GT,
       anon_sym_u21d2,
       anon_sym_COMMA,
       anon_sym_COLON_EQ,
-  [489] = 5,
+  [1085] = 3,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    ACTIONS(93), 2,
+      sym_identifier,
+      anon_sym_end,
+    ACTIONS(84), 6,
+      anon_sym_LPAREN,
+      sym_star,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+  [1102] = 3,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    ACTIONS(95), 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,
+  [1119] = 3,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    ACTIONS(97), 2,
+      sym_identifier,
+      anon_sym_end,
+    ACTIONS(82), 6,
+      anon_sym_LPAREN,
+      sym_star,
+      anon_sym_u25a1,
+      anon_sym_LBRACK_RBRACK,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+  [1136] = 5,
+    ACTIONS(99), 1,
+      ts_builtin_sym_end,
+    ACTIONS(101), 1,
+      sym_identifier,
+    ACTIONS(104), 1,
+      sym_command,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    STATE(29), 3,
+      sym_definition,
+      sym_preprocess,
+      aux_sym_program_repeat1,
+  [1155] = 2,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    ACTIONS(107), 6,
+      anon_sym_RPAREN,
+      anon_sym_COLON_EQ,
+      anon_sym_end,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+      anon_sym_SEMI,
+  [1168] = 3,
+    ACTIONS(111), 1,
+      anon_sym_COLON,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    ACTIONS(109), 5,
+      anon_sym_LPAREN,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+      anon_sym_COMMA,
+      anon_sym_COLON_EQ,
+  [1183] = 6,
+    ACTIONS(113), 1,
+      anon_sym_LPAREN,
+    ACTIONS(115), 1,
+      anon_sym_COLON,
+    ACTIONS(117), 1,
+      anon_sym_COLON_EQ,
+    STATE(69), 1,
+      sym_ascription,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    STATE(34), 2,
+      sym_param_block,
+      aux_sym_labs_repeat1,
+  [1204] = 2,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    ACTIONS(119), 6,
+      anon_sym_RPAREN,
+      anon_sym_COLON_EQ,
+      anon_sym_end,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+      anon_sym_SEMI,
+  [1217] = 6,
+    ACTIONS(113), 1,
+      anon_sym_LPAREN,
+    ACTIONS(115), 1,
+      anon_sym_COLON,
+    ACTIONS(121), 1,
+      anon_sym_COLON_EQ,
+    STATE(65), 1,
+      sym_ascription,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    STATE(25), 2,
+      sym_param_block,
+      aux_sym_labs_repeat1,
+  [1238] = 2,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    ACTIONS(123), 6,
+      anon_sym_RPAREN,
+      anon_sym_COLON_EQ,
+      anon_sym_end,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+      anon_sym_SEMI,
+  [1251] = 3,
+    ACTIONS(127), 1,
+      anon_sym_COLON,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    ACTIONS(125), 5,
+      anon_sym_LPAREN,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+      anon_sym_COMMA,
+      anon_sym_COLON_EQ,
+  [1266] = 5,
     ACTIONS(7), 1,
       sym_identifier,
     ACTIONS(9), 1,
       sym_command,
-    ACTIONS(59), 1,
+    ACTIONS(129), 1,
       ts_builtin_sym_end,
     ACTIONS(3), 2,
       sym_comment,
       sym_block_comment,
-    STATE(22), 3,
+    STATE(29), 3,
       sym_definition,
       sym_preprocess,
       aux_sym_program_repeat1,
-  [508] = 6,
-    ACTIONS(61), 1,
-      anon_sym_LPAREN,
-    ACTIONS(63), 1,
-      anon_sym_COLON,
-    ACTIONS(65), 1,
+  [1285] = 2,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    ACTIONS(131), 6,
+      anon_sym_RPAREN,
       anon_sym_COLON_EQ,
-    STATE(44), 1,
-      sym_ascription,
+      anon_sym_end,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+      anon_sym_SEMI,
+  [1298] = 2,
     ACTIONS(3), 2,
       sym_comment,
       sym_block_comment,
-    STATE(20), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-  [529] = 6,
-    ACTIONS(61), 1,
-      anon_sym_LPAREN,
-    ACTIONS(63), 1,
-      anon_sym_COLON,
-    ACTIONS(67), 1,
+    ACTIONS(133), 6,
+      anon_sym_RPAREN,
       anon_sym_COLON_EQ,
-    STATE(42), 1,
-      sym_ascription,
+      anon_sym_end,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+      anon_sym_SEMI,
+  [1311] = 2,
     ACTIONS(3), 2,
       sym_comment,
       sym_block_comment,
-    STATE(17), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-  [550] = 3,
-    ACTIONS(71), 1,
-      anon_sym_COLON,
-    ACTIONS(3), 2,
-      sym_comment,
-      sym_block_comment,
-    ACTIONS(69), 5,
+    ACTIONS(135), 6,
+      anon_sym_RPAREN,
+      anon_sym_COLON_EQ,
+      anon_sym_end,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+      anon_sym_SEMI,
+  [1324] = 4,
+    ACTIONS(113), 1,
       anon_sym_LPAREN,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    ACTIONS(137), 2,
       anon_sym_EQ_GT,
       anon_sym_u21d2,
-      anon_sym_COMMA,
+    STATE(25), 2,
+      sym_param_block,
+      aux_sym_labs_repeat1,
+  [1340] = 3,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    ACTIONS(139), 2,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+    ACTIONS(107), 3,
+      anon_sym_RPAREN,
       anon_sym_COLON_EQ,
-  [565] = 5,
-    ACTIONS(73), 1,
-      ts_builtin_sym_end,
-    ACTIONS(75), 1,
+      anon_sym_SEMI,
+  [1354] = 4,
+    ACTIONS(113), 1,
+      anon_sym_LPAREN,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    ACTIONS(141), 2,
+      anon_sym_EQ_GT,
+      anon_sym_u21d2,
+    STATE(25), 2,
+      sym_param_block,
+      aux_sym_labs_repeat1,
+  [1370] = 4,
+    ACTIONS(113), 1,
+      anon_sym_LPAREN,
+    ACTIONS(143), 1,
+      anon_sym_COMMA,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    STATE(25), 2,
+      sym_param_block,
+      aux_sym_labs_repeat1,
+  [1385] = 4,
+    ACTIONS(145), 1,
+      anon_sym_LPAREN,
+    ACTIONS(147), 1,
+      anon_sym_in,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    STATE(46), 2,
+      sym_binding,
+      aux_sym_let_repeat1,
+  [1400] = 4,
+    ACTIONS(149), 1,
+      anon_sym_LPAREN,
+    ACTIONS(152), 1,
+      anon_sym_in,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    STATE(46), 2,
+      sym_binding,
+      aux_sym_let_repeat1,
+  [1415] = 4,
+    ACTIONS(113), 1,
+      anon_sym_LPAREN,
+    ACTIONS(154), 1,
+      anon_sym_COMMA,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    STATE(25), 2,
+      sym_param_block,
+      aux_sym_labs_repeat1,
+  [1430] = 3,
+    ACTIONS(113), 1,
+      anon_sym_LPAREN,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    STATE(44), 2,
+      sym_param_block,
+      aux_sym_labs_repeat1,
+  [1442] = 4,
+    ACTIONS(156), 1,
       sym_identifier,
-    ACTIONS(78), 1,
-      sym_command,
-    ACTIONS(3), 2,
-      sym_comment,
-      sym_block_comment,
-    STATE(22), 3,
-      sym_definition,
-      sym_preprocess,
-      aux_sym_program_repeat1,
-  [584] = 3,
-    ACTIONS(83), 1,
+    ACTIONS(158), 1,
       anon_sym_COLON,
-    ACTIONS(3), 2,
-      sym_comment,
-      sym_block_comment,
-    ACTIONS(81), 5,
-      anon_sym_LPAREN,
-      anon_sym_EQ_GT,
-      anon_sym_u21d2,
-      anon_sym_COMMA,
-      anon_sym_COLON_EQ,
-  [599] = 3,
-    ACTIONS(3), 2,
-      sym_comment,
-      sym_block_comment,
-    ACTIONS(87), 2,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-    ACTIONS(85), 3,
-      anon_sym_RPAREN,
-      anon_sym_COLON_EQ,
-      anon_sym_SEMI,
-  [613] = 2,
-    ACTIONS(3), 2,
-      sym_comment,
-      sym_block_comment,
-    ACTIONS(85), 5,
-      anon_sym_RPAREN,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-      anon_sym_COLON_EQ,
-      anon_sym_SEMI,
-  [625] = 2,
-    ACTIONS(3), 2,
-      sym_comment,
-      sym_block_comment,
-    ACTIONS(89), 5,
-      anon_sym_RPAREN,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-      anon_sym_COLON_EQ,
-      anon_sym_SEMI,
-  [637] = 4,
-    ACTIONS(61), 1,
-      anon_sym_LPAREN,
-    ACTIONS(3), 2,
-      sym_comment,
-      sym_block_comment,
-    ACTIONS(91), 2,
-      anon_sym_EQ_GT,
-      anon_sym_u21d2,
-    STATE(17), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-  [653] = 2,
-    ACTIONS(3), 2,
-      sym_comment,
-      sym_block_comment,
-    ACTIONS(93), 5,
-      anon_sym_RPAREN,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-      anon_sym_COLON_EQ,
-      anon_sym_SEMI,
-  [665] = 2,
-    ACTIONS(3), 2,
-      sym_comment,
-      sym_block_comment,
-    ACTIONS(95), 5,
-      anon_sym_RPAREN,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-      anon_sym_COLON_EQ,
-      anon_sym_SEMI,
-  [677] = 2,
-    ACTIONS(3), 2,
-      sym_comment,
-      sym_block_comment,
-    ACTIONS(97), 5,
-      anon_sym_RPAREN,
-      anon_sym_DASH_GT,
-      anon_sym_u2192,
-      anon_sym_COLON_EQ,
-      anon_sym_SEMI,
-  [689] = 4,
-    ACTIONS(61), 1,
-      anon_sym_LPAREN,
-    ACTIONS(99), 1,
-      anon_sym_COMMA,
-    ACTIONS(3), 2,
-      sym_comment,
-      sym_block_comment,
-    STATE(17), 2,
-      sym_param_block,
-      aux_sym_labs_repeat1,
-  [704] = 4,
-    ACTIONS(101), 1,
-      sym_identifier,
-    ACTIONS(103), 1,
-      anon_sym_COLON,
-    STATE(36), 1,
+    STATE(56), 1,
       aux_sym_param_block_repeat1,
     ACTIONS(3), 2,
       sym_comment,
       sym_block_comment,
-  [718] = 3,
-    ACTIONS(61), 1,
+  [1456] = 2,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    ACTIONS(160), 3,
+      ts_builtin_sym_end,
+      sym_identifier,
+      sym_command,
+  [1466] = 2,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    ACTIONS(162), 3,
+      ts_builtin_sym_end,
+      sym_identifier,
+      sym_command,
+  [1476] = 4,
+    ACTIONS(164), 1,
+      sym_identifier,
+    ACTIONS(166), 1,
+      anon_sym_COLON,
+    STATE(49), 1,
+      aux_sym_param_block_repeat1,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+  [1490] = 2,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    ACTIONS(168), 3,
+      ts_builtin_sym_end,
+      sym_identifier,
+      sym_command,
+  [1500] = 3,
+    ACTIONS(113), 1,
       anon_sym_LPAREN,
     ACTIONS(3), 2,
       sym_comment,
       sym_block_comment,
-    STATE(27), 2,
+    STATE(41), 2,
       sym_param_block,
       aux_sym_labs_repeat1,
-  [730] = 4,
-    ACTIONS(105), 1,
+  [1512] = 2,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    ACTIONS(170), 3,
+      ts_builtin_sym_end,
       sym_identifier,
+      sym_command,
+  [1522] = 4,
+    ACTIONS(172), 1,
+      sym_identifier,
+    ACTIONS(175), 1,
+      anon_sym_COLON,
+    STATE(56), 1,
+      aux_sym_param_block_repeat1,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+  [1536] = 3,
     ACTIONS(107), 1,
-      anon_sym_COLON,
-    STATE(32), 1,
-      aux_sym_param_block_repeat1,
+      anon_sym_end,
     ACTIONS(3), 2,
       sym_comment,
       sym_block_comment,
-  [744] = 3,
-    ACTIONS(61), 1,
+    ACTIONS(177), 2,
+      anon_sym_DASH_GT,
+      anon_sym_u2192,
+  [1548] = 3,
+    ACTIONS(145), 1,
       anon_sym_LPAREN,
     ACTIONS(3), 2,
       sym_comment,
       sym_block_comment,
-    STATE(31), 2,
+    STATE(45), 2,
+      sym_binding,
+      aux_sym_let_repeat1,
+  [1560] = 3,
+    ACTIONS(113), 1,
+      anon_sym_LPAREN,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+    STATE(43), 2,
       sym_param_block,
       aux_sym_labs_repeat1,
-  [756] = 4,
-    ACTIONS(109), 1,
-      sym_identifier,
-    ACTIONS(112), 1,
-      anon_sym_COLON,
-    STATE(36), 1,
-      aux_sym_param_block_repeat1,
+  [1572] = 3,
+    ACTIONS(113), 1,
+      anon_sym_LPAREN,
     ACTIONS(3), 2,
       sym_comment,
       sym_block_comment,
-  [770] = 2,
+    STATE(47), 2,
+      sym_param_block,
+      aux_sym_labs_repeat1,
+  [1584] = 2,
     ACTIONS(3), 2,
       sym_comment,
       sym_block_comment,
-    ACTIONS(114), 3,
-      ts_builtin_sym_end,
-      sym_identifier,
-      sym_command,
-  [780] = 2,
-    ACTIONS(3), 2,
-      sym_comment,
-      sym_block_comment,
-    ACTIONS(116), 3,
-      ts_builtin_sym_end,
-      sym_identifier,
-      sym_command,
-  [790] = 2,
-    ACTIONS(3), 2,
-      sym_comment,
-      sym_block_comment,
-    ACTIONS(118), 3,
-      ts_builtin_sym_end,
-      sym_identifier,
-      sym_command,
-  [800] = 2,
-    ACTIONS(3), 2,
-      sym_comment,
-      sym_block_comment,
-    ACTIONS(120), 3,
-      ts_builtin_sym_end,
-      sym_identifier,
-      sym_command,
-  [810] = 2,
-    ACTIONS(122), 1,
-      anon_sym_RPAREN,
-    ACTIONS(3), 2,
-      sym_comment,
-      sym_block_comment,
-  [818] = 2,
-    ACTIONS(124), 1,
-      anon_sym_COLON_EQ,
-    ACTIONS(3), 2,
-      sym_comment,
-      sym_block_comment,
-  [826] = 2,
-    ACTIONS(126), 1,
+    ACTIONS(179), 2,
+      anon_sym_LPAREN,
+      anon_sym_in,
+  [1593] = 2,
+    ACTIONS(181), 1,
       anon_sym_SEMI,
     ACTIONS(3), 2,
       sym_comment,
       sym_block_comment,
-  [834] = 2,
-    ACTIONS(67), 1,
+  [1601] = 2,
+    ACTIONS(183), 1,
       anon_sym_COLON_EQ,
     ACTIONS(3), 2,
       sym_comment,
       sym_block_comment,
-  [842] = 2,
-    ACTIONS(128), 1,
-      ts_builtin_sym_end,
+  [1609] = 2,
+    ACTIONS(185), 1,
+      sym_identifier,
     ACTIONS(3), 2,
       sym_comment,
       sym_block_comment,
-  [850] = 2,
-    ACTIONS(132), 1,
+  [1617] = 2,
+    ACTIONS(187), 1,
+      anon_sym_COLON_EQ,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+  [1625] = 2,
+    ACTIONS(189), 1,
+      anon_sym_SEMI,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+  [1633] = 2,
+    ACTIONS(191), 1,
+      anon_sym_end,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+  [1641] = 2,
+    ACTIONS(193), 1,
+      anon_sym_RPAREN,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+  [1649] = 2,
+    ACTIONS(121), 1,
+      anon_sym_COLON_EQ,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+  [1657] = 2,
+    ACTIONS(195), 1,
+      anon_sym_RPAREN,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+  [1665] = 2,
+    ACTIONS(197), 1,
+      anon_sym_SEMI,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+  [1673] = 2,
+    ACTIONS(201), 1,
       sym_post_command,
-    ACTIONS(130), 2,
+    ACTIONS(199), 2,
       sym_comment,
       sym_block_comment,
-  [858] = 2,
-    ACTIONS(134), 1,
-      anon_sym_SEMI,
+  [1681] = 2,
+    ACTIONS(203), 1,
+      anon_sym_RPAREN,
     ACTIONS(3), 2,
       sym_comment,
       sym_block_comment,
-  [866] = 2,
-    ACTIONS(136), 1,
-      anon_sym_SEMI,
+  [1689] = 2,
+    ACTIONS(205), 1,
+      anon_sym_RPAREN,
     ACTIONS(3), 2,
       sym_comment,
       sym_block_comment,
-  [874] = 2,
-    ACTIONS(138), 1,
+  [1697] = 2,
+    ACTIONS(207), 1,
+      ts_builtin_sym_end,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+  [1705] = 2,
+    ACTIONS(209), 1,
+      anon_sym_RPAREN,
+    ACTIONS(3), 2,
+      sym_comment,
+      sym_block_comment,
+  [1713] = 2,
+    ACTIONS(211), 1,
       anon_sym_COLON_EQ,
     ACTIONS(3), 2,
       sym_comment,
       sym_block_comment,
-  [882] = 2,
-    ACTIONS(140), 1,
-      anon_sym_RPAREN,
-    ACTIONS(3), 2,
-      sym_comment,
-      sym_block_comment,
-  [890] = 2,
-    ACTIONS(142), 1,
-      anon_sym_RPAREN,
-    ACTIONS(3), 2,
-      sym_comment,
-      sym_block_comment,
 };
 
 static const uint32_t ts_small_parse_table_map[] = {
-  [SMALL_STATE(5)] = 0,
-  [SMALL_STATE(6)] = 51,
-  [SMALL_STATE(7)] = 102,
-  [SMALL_STATE(8)] = 153,
-  [SMALL_STATE(9)] = 204,
-  [SMALL_STATE(10)] = 255,
-  [SMALL_STATE(11)] = 306,
-  [SMALL_STATE(12)] = 357,
-  [SMALL_STATE(13)] = 387,
-  [SMALL_STATE(14)] = 417,
-  [SMALL_STATE(15)] = 434,
-  [SMALL_STATE(16)] = 451,
-  [SMALL_STATE(17)] = 468,
-  [SMALL_STATE(18)] = 489,
-  [SMALL_STATE(19)] = 508,
-  [SMALL_STATE(20)] = 529,
-  [SMALL_STATE(21)] = 550,
-  [SMALL_STATE(22)] = 565,
-  [SMALL_STATE(23)] = 584,
-  [SMALL_STATE(24)] = 599,
-  [SMALL_STATE(25)] = 613,
-  [SMALL_STATE(26)] = 625,
-  [SMALL_STATE(27)] = 637,
-  [SMALL_STATE(28)] = 653,
-  [SMALL_STATE(29)] = 665,
-  [SMALL_STATE(30)] = 677,
-  [SMALL_STATE(31)] = 689,
-  [SMALL_STATE(32)] = 704,
-  [SMALL_STATE(33)] = 718,
-  [SMALL_STATE(34)] = 730,
-  [SMALL_STATE(35)] = 744,
-  [SMALL_STATE(36)] = 756,
-  [SMALL_STATE(37)] = 770,
-  [SMALL_STATE(38)] = 780,
-  [SMALL_STATE(39)] = 790,
-  [SMALL_STATE(40)] = 800,
-  [SMALL_STATE(41)] = 810,
-  [SMALL_STATE(42)] = 818,
-  [SMALL_STATE(43)] = 826,
-  [SMALL_STATE(44)] = 834,
-  [SMALL_STATE(45)] = 842,
-  [SMALL_STATE(46)] = 850,
-  [SMALL_STATE(47)] = 858,
-  [SMALL_STATE(48)] = 866,
-  [SMALL_STATE(49)] = 874,
-  [SMALL_STATE(50)] = 882,
-  [SMALL_STATE(51)] = 890,
+  [SMALL_STATE(2)] = 0,
+  [SMALL_STATE(3)] = 58,
+  [SMALL_STATE(4)] = 116,
+  [SMALL_STATE(5)] = 174,
+  [SMALL_STATE(6)] = 229,
+  [SMALL_STATE(7)] = 284,
+  [SMALL_STATE(8)] = 339,
+  [SMALL_STATE(9)] = 394,
+  [SMALL_STATE(10)] = 449,
+  [SMALL_STATE(11)] = 504,
+  [SMALL_STATE(12)] = 559,
+  [SMALL_STATE(13)] = 614,
+  [SMALL_STATE(14)] = 669,
+  [SMALL_STATE(15)] = 724,
+  [SMALL_STATE(16)] = 779,
+  [SMALL_STATE(17)] = 834,
+  [SMALL_STATE(18)] = 889,
+  [SMALL_STATE(19)] = 919,
+  [SMALL_STATE(20)] = 949,
+  [SMALL_STATE(21)] = 981,
+  [SMALL_STATE(22)] = 1013,
+  [SMALL_STATE(23)] = 1030,
+  [SMALL_STATE(24)] = 1047,
+  [SMALL_STATE(25)] = 1064,
+  [SMALL_STATE(26)] = 1085,
+  [SMALL_STATE(27)] = 1102,
+  [SMALL_STATE(28)] = 1119,
+  [SMALL_STATE(29)] = 1136,
+  [SMALL_STATE(30)] = 1155,
+  [SMALL_STATE(31)] = 1168,
+  [SMALL_STATE(32)] = 1183,
+  [SMALL_STATE(33)] = 1204,
+  [SMALL_STATE(34)] = 1217,
+  [SMALL_STATE(35)] = 1238,
+  [SMALL_STATE(36)] = 1251,
+  [SMALL_STATE(37)] = 1266,
+  [SMALL_STATE(38)] = 1285,
+  [SMALL_STATE(39)] = 1298,
+  [SMALL_STATE(40)] = 1311,
+  [SMALL_STATE(41)] = 1324,
+  [SMALL_STATE(42)] = 1340,
+  [SMALL_STATE(43)] = 1354,
+  [SMALL_STATE(44)] = 1370,
+  [SMALL_STATE(45)] = 1385,
+  [SMALL_STATE(46)] = 1400,
+  [SMALL_STATE(47)] = 1415,
+  [SMALL_STATE(48)] = 1430,
+  [SMALL_STATE(49)] = 1442,
+  [SMALL_STATE(50)] = 1456,
+  [SMALL_STATE(51)] = 1466,
+  [SMALL_STATE(52)] = 1476,
+  [SMALL_STATE(53)] = 1490,
+  [SMALL_STATE(54)] = 1500,
+  [SMALL_STATE(55)] = 1512,
+  [SMALL_STATE(56)] = 1522,
+  [SMALL_STATE(57)] = 1536,
+  [SMALL_STATE(58)] = 1548,
+  [SMALL_STATE(59)] = 1560,
+  [SMALL_STATE(60)] = 1572,
+  [SMALL_STATE(61)] = 1584,
+  [SMALL_STATE(62)] = 1593,
+  [SMALL_STATE(63)] = 1601,
+  [SMALL_STATE(64)] = 1609,
+  [SMALL_STATE(65)] = 1617,
+  [SMALL_STATE(66)] = 1625,
+  [SMALL_STATE(67)] = 1633,
+  [SMALL_STATE(68)] = 1641,
+  [SMALL_STATE(69)] = 1649,
+  [SMALL_STATE(70)] = 1657,
+  [SMALL_STATE(71)] = 1665,
+  [SMALL_STATE(72)] = 1673,
+  [SMALL_STATE(73)] = 1681,
+  [SMALL_STATE(74)] = 1689,
+  [SMALL_STATE(75)] = 1697,
+  [SMALL_STATE(76)] = 1705,
+  [SMALL_STATE(77)] = 1713,
 };
 
 static const TSParseActionEntry ts_parse_actions[] = {
@@ -1656,71 +2456,103 @@ 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(19),
-  [9] = {.entry = {.count = 1, .reusable = true}}, SHIFT(46),
-  [11] = {.entry = {.count = 1, .reusable = false}}, SHIFT(14),
-  [13] = {.entry = {.count = 1, .reusable = true}}, SHIFT(6),
-  [15] = {.entry = {.count = 1, .reusable = true}}, SHIFT(14),
-  [17] = {.entry = {.count = 1, .reusable = true}}, SHIFT(15),
-  [19] = {.entry = {.count = 1, .reusable = true}}, SHIFT(33),
-  [21] = {.entry = {.count = 1, .reusable = false}}, SHIFT(33),
-  [23] = {.entry = {.count = 1, .reusable = true}}, SHIFT(35),
-  [25] = {.entry = {.count = 1, .reusable = false}}, SHIFT(35),
-  [27] = {.entry = {.count = 1, .reusable = false}}, SHIFT(43),
-  [29] = {.entry = {.count = 1, .reusable = false}}, SHIFT(48),
-  [31] = {.entry = {.count = 1, .reusable = false}}, SHIFT(47),
-  [33] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_app, 1, 0, 0),
-  [35] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(14),
-  [38] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(6),
-  [41] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0),
-  [43] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(15),
-  [46] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_term, 1, 0, 0),
-  [48] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_square, 1, 0, 0),
-  [50] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_term, 3, 0, 0),
-  [52] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_labs_repeat1, 2, 0, 0), SHIFT_REPEAT(34),
-  [55] = {.entry = {.count = 1, .reusable = false}}, REDUCE(aux_sym_labs_repeat1, 2, 0, 0),
-  [57] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_labs_repeat1, 2, 0, 0),
-  [59] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_program, 1, 0, 0),
-  [61] = {.entry = {.count = 1, .reusable = true}}, SHIFT(34),
-  [63] = {.entry = {.count = 1, .reusable = false}}, SHIFT(5),
-  [65] = {.entry = {.count = 1, .reusable = true}}, SHIFT(2),
-  [67] = {.entry = {.count = 1, .reusable = true}}, SHIFT(3),
-  [69] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_param_block, 5, 0, 4),
-  [71] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_param_block, 5, 0, 4),
-  [73] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0),
-  [75] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(19),
-  [78] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(46),
-  [81] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_param_block, 4, 0, 3),
-  [83] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_param_block, 4, 0, 3),
-  [85] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_expr, 1, 0, 0),
-  [87] = {.entry = {.count = 1, .reusable = true}}, SHIFT(9),
-  [89] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_app_term, 1, 0, 0),
-  [91] = {.entry = {.count = 1, .reusable = true}}, SHIFT(10),
-  [93] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_labs, 4, 0, 0),
-  [95] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_pabs, 4, 0, 0),
-  [97] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_arrow, 3, 0, 0),
-  [99] = {.entry = {.count = 1, .reusable = true}}, SHIFT(11),
-  [101] = {.entry = {.count = 1, .reusable = true}}, SHIFT(36),
-  [103] = {.entry = {.count = 1, .reusable = true}}, SHIFT(8),
-  [105] = {.entry = {.count = 1, .reusable = true}}, SHIFT(32),
-  [107] = {.entry = {.count = 1, .reusable = true}}, SHIFT(7),
-  [109] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_param_block_repeat1, 2, 0, 0), SHIFT_REPEAT(36),
-  [112] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_param_block_repeat1, 2, 0, 0),
-  [114] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 5, 0, 2),
-  [116] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 4, 0, 2),
-  [118] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_preprocess, 2, 0, 0),
-  [120] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 6, 0, 2),
-  [122] = {.entry = {.count = 1, .reusable = true}}, SHIFT(23),
-  [124] = {.entry = {.count = 1, .reusable = true}}, SHIFT(4),
-  [126] = {.entry = {.count = 1, .reusable = true}}, SHIFT(38),
-  [128] = {.entry = {.count = 1, .reusable = true}},  ACCEPT_INPUT(),
-  [130] = {.entry = {.count = 1, .reusable = false}}, SHIFT_EXTRA(),
-  [132] = {.entry = {.count = 1, .reusable = false}}, SHIFT(39),
-  [134] = {.entry = {.count = 1, .reusable = true}}, SHIFT(40),
-  [136] = {.entry = {.count = 1, .reusable = true}}, SHIFT(37),
-  [138] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_ascription, 2, 0, 1),
-  [140] = {.entry = {.count = 1, .reusable = true}}, SHIFT(16),
-  [142] = {.entry = {.count = 1, .reusable = true}}, SHIFT(21),
+  [7] = {.entry = {.count = 1, .reusable = true}}, SHIFT(32),
+  [9] = {.entry = {.count = 1, .reusable = true}}, SHIFT(72),
+  [11] = {.entry = {.count = 1, .reusable = false}}, SHIFT(24),
+  [13] = {.entry = {.count = 1, .reusable = true}}, SHIFT(7),
+  [15] = {.entry = {.count = 1, .reusable = true}}, SHIFT(24),
+  [17] = {.entry = {.count = 1, .reusable = true}}, SHIFT(23),
+  [19] = {.entry = {.count = 1, .reusable = true}}, SHIFT(54),
+  [21] = {.entry = {.count = 1, .reusable = false}}, SHIFT(54),
+  [23] = {.entry = {.count = 1, .reusable = true}}, SHIFT(48),
+  [25] = {.entry = {.count = 1, .reusable = false}}, SHIFT(48),
+  [27] = {.entry = {.count = 1, .reusable = false}}, SHIFT(58),
+  [29] = {.entry = {.count = 1, .reusable = false}}, SHIFT(71),
+  [31] = {.entry = {.count = 1, .reusable = false}}, SHIFT(66),
+  [33] = {.entry = {.count = 1, .reusable = false}}, SHIFT(62),
+  [35] = {.entry = {.count = 1, .reusable = false}}, SHIFT(26),
+  [37] = {.entry = {.count = 1, .reusable = true}}, SHIFT(17),
+  [39] = {.entry = {.count = 1, .reusable = true}}, SHIFT(26),
+  [41] = {.entry = {.count = 1, .reusable = true}}, SHIFT(28),
+  [43] = {.entry = {.count = 1, .reusable = true}}, SHIFT(59),
+  [45] = {.entry = {.count = 1, .reusable = false}}, SHIFT(59),
+  [47] = {.entry = {.count = 1, .reusable = true}}, SHIFT(60),
+  [49] = {.entry = {.count = 1, .reusable = false}}, SHIFT(60),
+  [51] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_app, 1, 0, 0),
+  [53] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(24),
+  [56] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(7),
+  [59] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0),
+  [61] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(23),
+  [64] = {.entry = {.count = 2, .reusable = false}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(26),
+  [67] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(17),
+  [70] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(26),
+  [73] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(28),
+  [76] = {.entry = {.count = 1, .reusable = false}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0),
+  [78] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_app, 1, 0, 0),
+  [80] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_term, 3, 0, 0),
+  [82] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_square, 1, 0, 0),
+  [84] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_term, 1, 0, 0),
+  [86] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_labs_repeat1, 2, 0, 0), SHIFT_REPEAT(52),
+  [89] = {.entry = {.count = 1, .reusable = false}}, REDUCE(aux_sym_labs_repeat1, 2, 0, 0),
+  [91] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_labs_repeat1, 2, 0, 0),
+  [93] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_term, 1, 0, 0),
+  [95] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_term, 3, 0, 0),
+  [97] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_square, 1, 0, 0),
+  [99] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0),
+  [101] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(32),
+  [104] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(72),
+  [107] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_expr, 1, 0, 0),
+  [109] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_param_block, 4, 0, 3),
+  [111] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_param_block, 4, 0, 3),
+  [113] = {.entry = {.count = 1, .reusable = true}}, SHIFT(52),
+  [115] = {.entry = {.count = 1, .reusable = false}}, SHIFT(6),
+  [117] = {.entry = {.count = 1, .reusable = true}}, SHIFT(3),
+  [119] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_arrow, 3, 0, 0),
+  [121] = {.entry = {.count = 1, .reusable = true}}, SHIFT(2),
+  [123] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_let, 5, 0, 0),
+  [125] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_param_block, 5, 0, 4),
+  [127] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_param_block, 5, 0, 4),
+  [129] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_program, 1, 0, 0),
+  [131] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_pabs, 4, 0, 0),
+  [133] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_labs, 4, 0, 0),
+  [135] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_app_term, 1, 0, 0),
+  [137] = {.entry = {.count = 1, .reusable = true}}, SHIFT(12),
+  [139] = {.entry = {.count = 1, .reusable = true}}, SHIFT(8),
+  [141] = {.entry = {.count = 1, .reusable = true}}, SHIFT(15),
+  [143] = {.entry = {.count = 1, .reusable = true}}, SHIFT(10),
+  [145] = {.entry = {.count = 1, .reusable = true}}, SHIFT(64),
+  [147] = {.entry = {.count = 1, .reusable = true}}, SHIFT(11),
+  [149] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_let_repeat1, 2, 0, 0), SHIFT_REPEAT(64),
+  [152] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_let_repeat1, 2, 0, 0),
+  [154] = {.entry = {.count = 1, .reusable = true}}, SHIFT(16),
+  [156] = {.entry = {.count = 1, .reusable = true}}, SHIFT(56),
+  [158] = {.entry = {.count = 1, .reusable = true}}, SHIFT(9),
+  [160] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 6, 0, 2),
+  [162] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 5, 0, 2),
+  [164] = {.entry = {.count = 1, .reusable = true}}, SHIFT(49),
+  [166] = {.entry = {.count = 1, .reusable = true}}, SHIFT(5),
+  [168] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 4, 0, 2),
+  [170] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_preprocess, 2, 0, 0),
+  [172] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_param_block_repeat1, 2, 0, 0), SHIFT_REPEAT(56),
+  [175] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_param_block_repeat1, 2, 0, 0),
+  [177] = {.entry = {.count = 1, .reusable = true}}, SHIFT(14),
+  [179] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_binding, 5, 0, 0),
+  [181] = {.entry = {.count = 1, .reusable = true}}, SHIFT(50),
+  [183] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_ascription, 2, 0, 1),
+  [185] = {.entry = {.count = 1, .reusable = true}}, SHIFT(77),
+  [187] = {.entry = {.count = 1, .reusable = true}}, SHIFT(4),
+  [189] = {.entry = {.count = 1, .reusable = true}}, SHIFT(53),
+  [191] = {.entry = {.count = 1, .reusable = true}}, SHIFT(35),
+  [193] = {.entry = {.count = 1, .reusable = true}}, SHIFT(22),
+  [195] = {.entry = {.count = 1, .reusable = true}}, SHIFT(61),
+  [197] = {.entry = {.count = 1, .reusable = true}}, SHIFT(51),
+  [199] = {.entry = {.count = 1, .reusable = false}}, SHIFT_EXTRA(),
+  [201] = {.entry = {.count = 1, .reusable = false}}, SHIFT(55),
+  [203] = {.entry = {.count = 1, .reusable = true}}, SHIFT(36),
+  [205] = {.entry = {.count = 1, .reusable = true}}, SHIFT(27),
+  [207] = {.entry = {.count = 1, .reusable = true}},  ACCEPT_INPUT(),
+  [209] = {.entry = {.count = 1, .reusable = true}}, SHIFT(31),
+  [211] = {.entry = {.count = 1, .reusable = true}}, SHIFT(13),
 };
 
 #ifdef __cplusplus
diff --git a/test/corpus/let.txt b/test/corpus/let.txt
new file mode 100644
index 0000000..bddcb71
--- /dev/null
+++ b/test/corpus/let.txt
@@ -0,0 +1,37 @@
+===
+Let
+===
+
+foo := let (x := a)
+           (y := x)
+       in
+           x
+       end;
+
+---
+
+(program
+  (definition
+    (identifier)
+    (expr
+      (app_term
+        (let
+          (binding
+            (identifier)
+            (expr
+              (app_term
+                (app
+                  (term
+                    (identifier))))))
+          (binding
+            (identifier)
+            (expr
+              (app_term
+                (app
+                  (term
+                    (identifier))))))
+          (expr
+            (app_term
+              (app
+                (term
+                  (identifier))))))))))