Constant tree_sitter_tlaplus::NODE_TYPES
source · pub const NODE_TYPES: &str = "[\n {\n \"type\": \"_expr\",\n \"named\": true,\n \"subtypes\": [\n {\n \"type\": \"_number\",\n \"named\": true\n },\n {\n \"type\": \"_primitive_value_set\",\n \"named\": true\n },\n {\n \"type\": \"boolean\",\n \"named\": true\n },\n {\n \"type\": \"bound_infix_op\",\n \"named\": true\n },\n {\n \"type\": \"bound_nonfix_op\",\n \"named\": true\n },\n {\n \"type\": \"bound_op\",\n \"named\": true\n },\n {\n \"type\": \"bound_postfix_op\",\n \"named\": true\n },\n {\n \"type\": \"bound_prefix_op\",\n \"named\": true\n },\n {\n \"type\": \"bounded_quantification\",\n \"named\": true\n },\n {\n \"type\": \"case\",\n \"named\": true\n },\n {\n \"type\": \"choose\",\n \"named\": true\n },\n {\n \"type\": \"conj_list\",\n \"named\": true\n },\n {\n \"type\": \"disj_list\",\n \"named\": true\n },\n {\n \"type\": \"except\",\n \"named\": true\n },\n {\n \"type\": \"fairness\",\n \"named\": true\n },\n {\n \"type\": \"finite_set_literal\",\n \"named\": true\n },\n {\n \"type\": \"function_evaluation\",\n \"named\": true\n },\n {\n \"type\": \"function_literal\",\n \"named\": true\n },\n {\n \"type\": \"identifier_ref\",\n \"named\": true\n },\n {\n \"type\": \"if_then_else\",\n \"named\": true\n },\n {\n \"type\": \"label\",\n \"named\": true\n },\n {\n \"type\": \"let_in\",\n \"named\": true\n },\n {\n \"type\": \"parentheses\",\n \"named\": true\n },\n {\n \"type\": \"prefixed_op\",\n \"named\": true\n },\n {\n \"type\": \"prev_func_val\",\n \"named\": true\n },\n {\n \"type\": \"proof_step_ref\",\n \"named\": true\n },\n {\n \"type\": \"record_literal\",\n \"named\": true\n },\n {\n \"type\": \"record_value\",\n \"named\": true\n },\n {\n \"type\": \"set_filter\",\n \"named\": true\n },\n {\n \"type\": \"set_map\",\n \"named\": true\n },\n {\n \"type\": \"set_of_functions\",\n \"named\": true\n },\n {\n \"type\": \"set_of_records\",\n \"named\": true\n },\n {\n \"type\": \"step_expr_no_stutter\",\n \"named\": true\n },\n {\n \"type\": \"step_expr_or_stutter\",\n \"named\": true\n },\n {\n \"type\": \"string\",\n \"named\": true\n },\n {\n \"type\": \"subexpression\",\n \"named\": true\n },\n {\n \"type\": \"tuple_literal\",\n \"named\": true\n },\n {\n \"type\": \"unbounded_quantification\",\n \"named\": true\n }\n ]\n },\n {\n \"type\": \"_number\",\n \"named\": true,\n \"subtypes\": [\n {\n \"type\": \"binary_number\",\n \"named\": true\n },\n {\n \"type\": \"hex_number\",\n \"named\": true\n },\n {\n \"type\": \"nat_number\",\n \"named\": true\n },\n {\n \"type\": \"octal_number\",\n \"named\": true\n },\n {\n \"type\": \"real_number\",\n \"named\": true\n }\n ]\n },\n {\n \"type\": \"_op\",\n \"named\": true,\n \"subtypes\": [\n {\n \"type\": \"infix_op_symbol\",\n \"named\": true\n },\n {\n \"type\": \"lambda\",\n \"named\": true\n },\n {\n \"type\": \"postfix_op_symbol\",\n \"named\": true\n },\n {\n \"type\": \"prefix_op_symbol\",\n \"named\": true\n }\n ]\n },\n {\n \"type\": \"_primitive_value_set\",\n \"named\": true,\n \"subtypes\": [\n {\n \"type\": \"boolean_set\",\n \"named\": true\n },\n {\n \"type\": \"int_number_set\",\n \"named\": true\n },\n {\n \"type\": \"nat_number_set\",\n \"named\": true\n },\n {\n \"type\": \"real_number_set\",\n \"named\": true\n },\n {\n \"type\": \"string_set\",\n \"named\": true\n }\n ]\n },\n {\n \"type\": \"_proof\",\n \"named\": true,\n \"subtypes\": [\n {\n \"type\": \"non_terminal_proof\",\n \"named\": true\n },\n {\n \"type\": \"terminal_proof\",\n \"named\": true\n }\n ]\n },\n {\n \"type\": \"_unit\",\n \"named\": true,\n \"subtypes\": [\n {\n \"type\": \"assumption\",\n \"named\": true\n },\n {\n \"type\": \"constant_declaration\",\n \"named\": true\n },\n {\n \"type\": \"function_definition\",\n \"named\": true\n },\n {\n \"type\": \"instance\",\n \"named\": true\n },\n {\n \"type\": \"local_definition\",\n \"named\": true\n },\n {\n \"type\": \"module\",\n \"named\": true\n },\n {\n \"type\": \"module_definition\",\n \"named\": true\n },\n {\n \"type\": \"operator_definition\",\n \"named\": true\n },\n {\n \"type\": \"recursive_declaration\",\n \"named\": true\n },\n {\n \"type\": \"single_line\",\n \"named\": true\n },\n {\n \"type\": \"theorem\",\n \"named\": true\n },\n {\n \"type\": \"use_or_hide\",\n \"named\": true\n },\n {\n \"type\": \"variable_declaration\",\n \"named\": true\n }\n ]\n },\n {\n \"type\": \"address\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"all_map_to\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"always\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"approx\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"assign\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"assume_prove\",\n \"named\": true,\n \"fields\": {\n \"assumption\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \",\",\n \"named\": false\n },\n {\n \"type\": \"_expr\",\n \"named\": true\n },\n {\n \"type\": \"inner_assume_prove\",\n \"named\": true\n },\n {\n \"type\": \"new\",\n \"named\": true\n }\n ]\n },\n \"conclusion\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n }\n }\n },\n {\n \"type\": \"assumption\",\n \"named\": true,\n \"fields\": {\n \"name\": {\n \"multiple\": false,\n \"required\": false,\n \"types\": [\n {\n \"type\": \"identifier\",\n \"named\": true\n }\n ]\n }\n },\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n },\n {\n \"type\": \"def_eq\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"asymp\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"bigcirc\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"binary_number\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"format\",\n \"named\": true\n },\n {\n \"type\": \"value\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"block_comment\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": false,\n \"types\": [\n {\n \"type\": \"block_comment_text\",\n \"named\": true\n },\n {\n \"type\": \"pcal_algorithm\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"block_comment_text\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"bnf_rule\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"boolean\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"bound_infix_op\",\n \"named\": true,\n \"fields\": {\n \"lhs\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n },\n \"rhs\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n },\n \"symbol\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"amp\",\n \"named\": true\n },\n {\n \"type\": \"ampamp\",\n \"named\": true\n },\n {\n \"type\": \"approx\",\n \"named\": true\n },\n {\n \"type\": \"assign\",\n \"named\": true\n },\n {\n \"type\": \"asymp\",\n \"named\": true\n },\n {\n \"type\": \"bigcirc\",\n \"named\": true\n },\n {\n \"type\": \"bnf_rule\",\n \"named\": true\n },\n {\n \"type\": \"bullet\",\n \"named\": true\n },\n {\n \"type\": \"cap\",\n \"named\": true\n },\n {\n \"type\": \"cdot\",\n \"named\": true\n },\n {\n \"type\": \"circ\",\n \"named\": true\n },\n {\n \"type\": \"compose\",\n \"named\": true\n },\n {\n \"type\": \"cong\",\n \"named\": true\n },\n {\n \"type\": \"cup\",\n \"named\": true\n },\n {\n \"type\": \"div\",\n \"named\": true\n },\n {\n \"type\": \"dol\",\n \"named\": true\n },\n {\n \"type\": \"doldol\",\n \"named\": true\n },\n {\n \"type\": \"doteq\",\n \"named\": true\n },\n {\n \"type\": \"dots_2\",\n \"named\": true\n },\n {\n \"type\": \"dots_3\",\n \"named\": true\n },\n {\n \"type\": \"eq\",\n \"named\": true\n },\n {\n \"type\": \"equiv\",\n \"named\": true\n },\n {\n \"type\": \"excl\",\n \"named\": true\n },\n {\n \"type\": \"geq\",\n \"named\": true\n },\n {\n \"type\": \"gg\",\n \"named\": true\n },\n {\n \"type\": \"gt\",\n \"named\": true\n },\n {\n \"type\": \"hashhash\",\n \"named\": true\n },\n {\n \"type\": \"iff\",\n \"named\": true\n },\n {\n \"type\": \"implies\",\n \"named\": true\n },\n {\n \"type\": \"in\",\n \"named\": true\n },\n {\n \"type\": \"land\",\n \"named\": true\n },\n {\n \"type\": \"ld_ttile\",\n \"named\": true\n },\n {\n \"type\": \"leads_to\",\n \"named\": true\n },\n {\n \"type\": \"leq\",\n \"named\": true\n },\n {\n \"type\": \"ll\",\n \"named\": true\n },\n {\n \"type\": \"lor\",\n \"named\": true\n },\n {\n \"type\": \"ls_ttile\",\n \"named\": true\n },\n {\n \"type\": \"lt\",\n \"named\": true\n },\n {\n \"type\": \"map_from\",\n \"named\": true\n },\n {\n \"type\": \"map_to\",\n \"named\": true\n },\n {\n \"type\": \"minus\",\n \"named\": true\n },\n {\n \"type\": \"minusminus\",\n \"named\": true\n },\n {\n \"type\": \"mod\",\n \"named\": true\n },\n {\n \"type\": \"modmod\",\n \"named\": true\n },\n {\n \"type\": \"mul\",\n \"named\": true\n },\n {\n \"type\": \"mulmul\",\n \"named\": true\n },\n {\n \"type\": \"neq\",\n \"named\": true\n },\n {\n \"type\": \"notin\",\n \"named\": true\n },\n {\n \"type\": \"odot\",\n \"named\": true\n },\n {\n \"type\": \"ominus\",\n \"named\": true\n },\n {\n \"type\": \"oplus\",\n \"named\": true\n },\n {\n \"type\": \"oslash\",\n \"named\": true\n },\n {\n \"type\": \"otimes\",\n \"named\": true\n },\n {\n \"type\": \"plus\",\n \"named\": true\n },\n {\n \"type\": \"plus_arrow\",\n \"named\": true\n },\n {\n \"type\": \"plusplus\",\n \"named\": true\n },\n {\n \"type\": \"pow\",\n \"named\": true\n },\n {\n \"type\": \"powpow\",\n \"named\": true\n },\n {\n \"type\": \"prec\",\n \"named\": true\n },\n {\n \"type\": \"preceq\",\n \"named\": true\n },\n {\n \"type\": \"propto\",\n \"named\": true\n },\n {\n \"type\": \"qq\",\n \"named\": true\n },\n {\n \"type\": \"rd_ttile\",\n \"named\": true\n },\n {\n \"type\": \"rs_ttile\",\n \"named\": true\n },\n {\n \"type\": \"setminus\",\n \"named\": true\n },\n {\n \"type\": \"sim\",\n \"named\": true\n },\n {\n \"type\": \"simeq\",\n \"named\": true\n },\n {\n \"type\": \"slash\",\n \"named\": true\n },\n {\n \"type\": \"slashslash\",\n \"named\": true\n },\n {\n \"type\": \"sqcap\",\n \"named\": true\n },\n {\n \"type\": \"sqcup\",\n \"named\": true\n },\n {\n \"type\": \"sqsubset\",\n \"named\": true\n },\n {\n \"type\": \"sqsubseteq\",\n \"named\": true\n },\n {\n \"type\": \"sqsupset\",\n \"named\": true\n },\n {\n \"type\": \"sqsupseteq\",\n \"named\": true\n },\n {\n \"type\": \"star\",\n \"named\": true\n },\n {\n \"type\": \"subset\",\n \"named\": true\n },\n {\n \"type\": \"subseteq\",\n \"named\": true\n },\n {\n \"type\": \"succ\",\n \"named\": true\n },\n {\n \"type\": \"succeq\",\n \"named\": true\n },\n {\n \"type\": \"supset\",\n \"named\": true\n },\n {\n \"type\": \"supseteq\",\n \"named\": true\n },\n {\n \"type\": \"times\",\n \"named\": true\n },\n {\n \"type\": \"uplus\",\n \"named\": true\n },\n {\n \"type\": \"vert\",\n \"named\": true\n },\n {\n \"type\": \"vertvert\",\n \"named\": true\n },\n {\n \"type\": \"wr\",\n \"named\": true\n }\n ]\n }\n }\n },\n {\n \"type\": \"bound_nonfix_op\",\n \"named\": true,\n \"fields\": {\n \"symbol\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"infix_op_symbol\",\n \"named\": true\n },\n {\n \"type\": \"postfix_op_symbol\",\n \"named\": true\n },\n {\n \"type\": \"prefix_op_symbol\",\n \"named\": true\n }\n ]\n }\n },\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"bound_op\",\n \"named\": true,\n \"fields\": {\n \"name\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"identifier_ref\",\n \"named\": true\n }\n ]\n },\n \"parameter\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"(\",\n \"named\": false\n },\n {\n \"type\": \")\",\n \"named\": false\n },\n {\n \"type\": \",\",\n \"named\": false\n },\n {\n \"type\": \"_expr\",\n \"named\": true\n },\n {\n \"type\": \"_op\",\n \"named\": true\n }\n ]\n }\n }\n },\n {\n \"type\": \"bound_postfix_op\",\n \"named\": true,\n \"fields\": {\n \"lhs\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n },\n \"symbol\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"asterisk\",\n \"named\": true\n },\n {\n \"type\": \"prime\",\n \"named\": true\n },\n {\n \"type\": \"sup_hash\",\n \"named\": true\n },\n {\n \"type\": \"sup_plus\",\n \"named\": true\n }\n ]\n }\n }\n },\n {\n \"type\": \"bound_prefix_op\",\n \"named\": true,\n \"fields\": {\n \"rhs\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n },\n \"symbol\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"always\",\n \"named\": true\n },\n {\n \"type\": \"domain\",\n \"named\": true\n },\n {\n \"type\": \"enabled\",\n \"named\": true\n },\n {\n \"type\": \"eventually\",\n \"named\": true\n },\n {\n \"type\": \"lnot\",\n \"named\": true\n },\n {\n \"type\": \"negative\",\n \"named\": true\n },\n {\n \"type\": \"powerset\",\n \"named\": true\n },\n {\n \"type\": \"unchanged\",\n \"named\": true\n },\n {\n \"type\": \"union\",\n \"named\": true\n }\n ]\n }\n }\n },\n {\n \"type\": \"bounded_quantification\",\n \"named\": true,\n \"fields\": {\n \"bound\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \",\",\n \"named\": false\n },\n {\n \"type\": \"quantifier_bound\",\n \"named\": true\n }\n ]\n },\n \"expression\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n },\n \"quantifier\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"exists\",\n \"named\": true\n },\n {\n \"type\": \"forall\",\n \"named\": true\n }\n ]\n }\n }\n },\n {\n \"type\": \"bullet\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"bullet_conj\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"bullet_disj\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"cap\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"case\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"case_arm\",\n \"named\": true\n },\n {\n \"type\": \"case_box\",\n \"named\": true\n },\n {\n \"type\": \"other_arm\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"case_arm\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n },\n {\n \"type\": \"case_arrow\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"case_arrow\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"case_box\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"case_proof_step\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n },\n {\n \"type\": \"_proof\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"cdot\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"child_id\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"choose\",\n \"named\": true,\n \"fields\": {\n \"expression\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n },\n \"intro\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"identifier\",\n \"named\": true\n },\n {\n \"type\": \"tuple_of_identifiers\",\n \"named\": true\n }\n ]\n },\n \"set\": {\n \"multiple\": false,\n \"required\": false,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n }\n },\n \"children\": {\n \"multiple\": false,\n \"required\": false,\n \"types\": [\n {\n \"type\": \"set_in\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"circ\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"colon\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"cong\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"conj_item\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n },\n {\n \"type\": \"bullet_conj\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"conj_list\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"conj_item\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"constant_declaration\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"identifier\",\n \"named\": true\n },\n {\n \"type\": \"operator_declaration\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"cup\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"def_eq\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"definition_proof_step\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"function_definition\",\n \"named\": true\n },\n {\n \"type\": \"module_definition\",\n \"named\": true\n },\n {\n \"type\": \"operator_definition\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"disj_item\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n },\n {\n \"type\": \"bullet_disj\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"disj_list\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"disj_item\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"div\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"domain\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"doteq\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"dots_2\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"dots_3\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"double_line\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"enabled\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"eq\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"equiv\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"eventually\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"except\",\n \"named\": true,\n \"fields\": {\n \"expr_to_update\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n }\n },\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"except_update\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"except_update\",\n \"named\": true,\n \"fields\": {\n \"new_val\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n },\n \"update_specifier\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"!\",\n \"named\": false\n },\n {\n \"type\": \"except_update_specifier\",\n \"named\": true\n }\n ]\n }\n }\n },\n {\n \"type\": \"except_update_fn_appl\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"except_update_record_field\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"identifier_ref\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"except_update_specifier\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"except_update_fn_appl\",\n \"named\": true\n },\n {\n \"type\": \"except_update_record_field\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"excl\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"exists\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"extends\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"identifier_ref\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"fair\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"fairness\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"finite_set_literal\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": false,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"forall\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"function_definition\",\n \"named\": true,\n \"fields\": {\n \"definition\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n },\n \"name\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"identifier\",\n \"named\": true\n }\n ]\n }\n },\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"def_eq\",\n \"named\": true\n },\n {\n \"type\": \"quantifier_bound\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"function_evaluation\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"function_literal\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n },\n {\n \"type\": \"all_map_to\",\n \"named\": true\n },\n {\n \"type\": \"quantifier_bound\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"geq\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"gets\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"gg\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"have_proof_step\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"header_line\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"hex_number\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"format\",\n \"named\": true\n },\n {\n \"type\": \"value\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"if_then_else\",\n \"named\": true,\n \"fields\": {\n \"else\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n },\n \"if\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n },\n \"then\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n }\n }\n },\n {\n \"type\": \"iff\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"implies\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"in\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"infix_op_symbol\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"amp\",\n \"named\": true\n },\n {\n \"type\": \"ampamp\",\n \"named\": true\n },\n {\n \"type\": \"approx\",\n \"named\": true\n },\n {\n \"type\": \"assign\",\n \"named\": true\n },\n {\n \"type\": \"asymp\",\n \"named\": true\n },\n {\n \"type\": \"bigcirc\",\n \"named\": true\n },\n {\n \"type\": \"bnf_rule\",\n \"named\": true\n },\n {\n \"type\": \"bullet\",\n \"named\": true\n },\n {\n \"type\": \"cap\",\n \"named\": true\n },\n {\n \"type\": \"cdot\",\n \"named\": true\n },\n {\n \"type\": \"circ\",\n \"named\": true\n },\n {\n \"type\": \"compose\",\n \"named\": true\n },\n {\n \"type\": \"cong\",\n \"named\": true\n },\n {\n \"type\": \"cup\",\n \"named\": true\n },\n {\n \"type\": \"div\",\n \"named\": true\n },\n {\n \"type\": \"dol\",\n \"named\": true\n },\n {\n \"type\": \"doldol\",\n \"named\": true\n },\n {\n \"type\": \"doteq\",\n \"named\": true\n },\n {\n \"type\": \"dots_2\",\n \"named\": true\n },\n {\n \"type\": \"dots_3\",\n \"named\": true\n },\n {\n \"type\": \"eq\",\n \"named\": true\n },\n {\n \"type\": \"equiv\",\n \"named\": true\n },\n {\n \"type\": \"excl\",\n \"named\": true\n },\n {\n \"type\": \"geq\",\n \"named\": true\n },\n {\n \"type\": \"gg\",\n \"named\": true\n },\n {\n \"type\": \"gt\",\n \"named\": true\n },\n {\n \"type\": \"hashhash\",\n \"named\": true\n },\n {\n \"type\": \"iff\",\n \"named\": true\n },\n {\n \"type\": \"implies\",\n \"named\": true\n },\n {\n \"type\": \"in\",\n \"named\": true\n },\n {\n \"type\": \"land\",\n \"named\": true\n },\n {\n \"type\": \"ld_ttile\",\n \"named\": true\n },\n {\n \"type\": \"leads_to\",\n \"named\": true\n },\n {\n \"type\": \"leq\",\n \"named\": true\n },\n {\n \"type\": \"ll\",\n \"named\": true\n },\n {\n \"type\": \"lor\",\n \"named\": true\n },\n {\n \"type\": \"ls_ttile\",\n \"named\": true\n },\n {\n \"type\": \"lt\",\n \"named\": true\n },\n {\n \"type\": \"map_from\",\n \"named\": true\n },\n {\n \"type\": \"map_to\",\n \"named\": true\n },\n {\n \"type\": \"minus\",\n \"named\": true\n },\n {\n \"type\": \"minusminus\",\n \"named\": true\n },\n {\n \"type\": \"mod\",\n \"named\": true\n },\n {\n \"type\": \"modmod\",\n \"named\": true\n },\n {\n \"type\": \"mul\",\n \"named\": true\n },\n {\n \"type\": \"mulmul\",\n \"named\": true\n },\n {\n \"type\": \"neq\",\n \"named\": true\n },\n {\n \"type\": \"notin\",\n \"named\": true\n },\n {\n \"type\": \"odot\",\n \"named\": true\n },\n {\n \"type\": \"ominus\",\n \"named\": true\n },\n {\n \"type\": \"oplus\",\n \"named\": true\n },\n {\n \"type\": \"oslash\",\n \"named\": true\n },\n {\n \"type\": \"otimes\",\n \"named\": true\n },\n {\n \"type\": \"plus\",\n \"named\": true\n },\n {\n \"type\": \"plus_arrow\",\n \"named\": true\n },\n {\n \"type\": \"plusplus\",\n \"named\": true\n },\n {\n \"type\": \"pow\",\n \"named\": true\n },\n {\n \"type\": \"powpow\",\n \"named\": true\n },\n {\n \"type\": \"prec\",\n \"named\": true\n },\n {\n \"type\": \"preceq\",\n \"named\": true\n },\n {\n \"type\": \"propto\",\n \"named\": true\n },\n {\n \"type\": \"qq\",\n \"named\": true\n },\n {\n \"type\": \"rd_ttile\",\n \"named\": true\n },\n {\n \"type\": \"rs_ttile\",\n \"named\": true\n },\n {\n \"type\": \"setminus\",\n \"named\": true\n },\n {\n \"type\": \"sim\",\n \"named\": true\n },\n {\n \"type\": \"simeq\",\n \"named\": true\n },\n {\n \"type\": \"slash\",\n \"named\": true\n },\n {\n \"type\": \"slashslash\",\n \"named\": true\n },\n {\n \"type\": \"sqcap\",\n \"named\": true\n },\n {\n \"type\": \"sqcup\",\n \"named\": true\n },\n {\n \"type\": \"sqsubset\",\n \"named\": true\n },\n {\n \"type\": \"sqsubseteq\",\n \"named\": true\n },\n {\n \"type\": \"sqsupset\",\n \"named\": true\n },\n {\n \"type\": \"sqsupseteq\",\n \"named\": true\n },\n {\n \"type\": \"star\",\n \"named\": true\n },\n {\n \"type\": \"subset\",\n \"named\": true\n },\n {\n \"type\": \"subseteq\",\n \"named\": true\n },\n {\n \"type\": \"succ\",\n \"named\": true\n },\n {\n \"type\": \"succeq\",\n \"named\": true\n },\n {\n \"type\": \"supset\",\n \"named\": true\n },\n {\n \"type\": \"supseteq\",\n \"named\": true\n },\n {\n \"type\": \"times\",\n \"named\": true\n },\n {\n \"type\": \"uplus\",\n \"named\": true\n },\n {\n \"type\": \"vert\",\n \"named\": true\n },\n {\n \"type\": \"vertvert\",\n \"named\": true\n },\n {\n \"type\": \"wr\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"inner_assume_prove\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"assume_prove\",\n \"named\": true\n },\n {\n \"type\": \"identifier\",\n \"named\": true\n },\n {\n \"type\": \"label_as\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"instance\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"identifier_ref\",\n \"named\": true\n },\n {\n \"type\": \"substitution\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"int_number_set\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"label\",\n \"named\": true,\n \"fields\": {\n \"expression\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n },\n \"name\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"identifier\",\n \"named\": true\n }\n ]\n },\n \"parameter\": {\n \"multiple\": true,\n \"required\": false,\n \"types\": [\n {\n \"type\": \"(\",\n \"named\": false\n },\n {\n \"type\": \")\",\n \"named\": false\n },\n {\n \"type\": \",\",\n \"named\": false\n },\n {\n \"type\": \"identifier_ref\",\n \"named\": true\n }\n ]\n }\n },\n \"children\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"label_as\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"label_as\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"lambda\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n },\n {\n \"type\": \"identifier\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"land\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"langle_bracket\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"ld_ttile\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"leads_to\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"leq\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"let_in\",\n \"named\": true,\n \"fields\": {\n \"definitions\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"function_definition\",\n \"named\": true\n },\n {\n \"type\": \"module_definition\",\n \"named\": true\n },\n {\n \"type\": \"operator_definition\",\n \"named\": true\n },\n {\n \"type\": \"recursive_declaration\",\n \"named\": true\n }\n ]\n },\n \"expression\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n }\n }\n },\n {\n \"type\": \"ll\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"lnot\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"local_definition\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"function_definition\",\n \"named\": true\n },\n {\n \"type\": \"instance\",\n \"named\": true\n },\n {\n \"type\": \"module_definition\",\n \"named\": true\n },\n {\n \"type\": \"operator_definition\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"lor\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"ls_ttile\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"lt\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"maps_to\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"minus\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"module\",\n \"named\": true,\n \"fields\": {\n \"name\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"identifier\",\n \"named\": true\n }\n ]\n }\n },\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_unit\",\n \"named\": true\n },\n {\n \"type\": \"double_line\",\n \"named\": true\n },\n {\n \"type\": \"extends\",\n \"named\": true\n },\n {\n \"type\": \"header_line\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"module_definition\",\n \"named\": true,\n \"fields\": {\n \"definition\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"instance\",\n \"named\": true\n }\n ]\n },\n \"name\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"identifier\",\n \"named\": true\n }\n ]\n },\n \"parameter\": {\n \"multiple\": true,\n \"required\": false,\n \"types\": [\n {\n \"type\": \"(\",\n \"named\": false\n },\n {\n \"type\": \")\",\n \"named\": false\n },\n {\n \"type\": \",\",\n \"named\": false\n },\n {\n \"type\": \"identifier\",\n \"named\": true\n },\n {\n \"type\": \"operator_declaration\",\n \"named\": true\n }\n ]\n }\n },\n \"children\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"def_eq\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"module_ref\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"identifier_ref\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"nat_number\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"nat_number_set\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"negative\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"neq\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"new\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n },\n {\n \"type\": \"identifier\",\n \"named\": true\n },\n {\n \"type\": \"operator_declaration\",\n \"named\": true\n },\n {\n \"type\": \"set_in\",\n \"named\": true\n },\n {\n \"type\": \"statement_level\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"non_terminal_proof\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"proof_step\",\n \"named\": true\n },\n {\n \"type\": \"qed_step\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"notin\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"octal_number\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"format\",\n \"named\": true\n },\n {\n \"type\": \"value\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"odot\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"ominus\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"operator_args\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n },\n {\n \"type\": \"_op\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"operator_declaration\",\n \"named\": true,\n \"fields\": {\n \"name\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"identifier\",\n \"named\": true\n },\n {\n \"type\": \"infix_op_symbol\",\n \"named\": true\n },\n {\n \"type\": \"postfix_op_symbol\",\n \"named\": true\n },\n {\n \"type\": \"prefix_op_symbol\",\n \"named\": true\n }\n ]\n },\n \"parameter\": {\n \"multiple\": true,\n \"required\": false,\n \"types\": [\n {\n \"type\": \"(\",\n \"named\": false\n },\n {\n \"type\": \")\",\n \"named\": false\n },\n {\n \"type\": \",\",\n \"named\": false\n },\n {\n \"type\": \"placeholder\",\n \"named\": true\n }\n ]\n }\n },\n \"children\": {\n \"multiple\": true,\n \"required\": false,\n \"types\": [\n {\n \"type\": \"placeholder\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"operator_definition\",\n \"named\": true,\n \"fields\": {\n \"definition\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n },\n \"name\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"identifier\",\n \"named\": true\n },\n {\n \"type\": \"infix_op_symbol\",\n \"named\": true\n },\n {\n \"type\": \"postfix_op_symbol\",\n \"named\": true\n },\n {\n \"type\": \"prefix_op_symbol\",\n \"named\": true\n }\n ]\n },\n \"parameter\": {\n \"multiple\": true,\n \"required\": false,\n \"types\": [\n {\n \"type\": \"(\",\n \"named\": false\n },\n {\n \"type\": \")\",\n \"named\": false\n },\n {\n \"type\": \",\",\n \"named\": false\n },\n {\n \"type\": \"identifier\",\n \"named\": true\n },\n {\n \"type\": \"operator_declaration\",\n \"named\": true\n }\n ]\n }\n },\n \"children\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"def_eq\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"oplus\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"oslash\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"other_arm\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n },\n {\n \"type\": \"case_arrow\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"otimes\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"parentheses\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"pcal_algorithm\",\n \"named\": true,\n \"fields\": {\n \"name\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"identifier\",\n \"named\": true\n }\n ]\n }\n },\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"pcal_algorithm_body\",\n \"named\": true\n },\n {\n \"type\": \"pcal_algorithm_start\",\n \"named\": true\n },\n {\n \"type\": \"pcal_definitions\",\n \"named\": true\n },\n {\n \"type\": \"pcal_macro\",\n \"named\": true\n },\n {\n \"type\": \"pcal_procedure\",\n \"named\": true\n },\n {\n \"type\": \"pcal_process\",\n \"named\": true\n },\n {\n \"type\": \"pcal_var_decls\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"pcal_algorithm_body\",\n \"named\": true,\n \"fields\": {\n \"label\": {\n \"multiple\": true,\n \"required\": false,\n \"types\": [\n {\n \"type\": \":\",\n \"named\": false\n },\n {\n \"type\": \"identifier\",\n \"named\": true\n }\n ]\n }\n },\n \"children\": {\n \"multiple\": true,\n \"required\": false,\n \"types\": [\n {\n \"type\": \"pcal_algorithm_body\",\n \"named\": true\n },\n {\n \"type\": \"pcal_assert\",\n \"named\": true\n },\n {\n \"type\": \"pcal_assign\",\n \"named\": true\n },\n {\n \"type\": \"pcal_await\",\n \"named\": true\n },\n {\n \"type\": \"pcal_either\",\n \"named\": true\n },\n {\n \"type\": \"pcal_goto\",\n \"named\": true\n },\n {\n \"type\": \"pcal_if\",\n \"named\": true\n },\n {\n \"type\": \"pcal_macro_call\",\n \"named\": true\n },\n {\n \"type\": \"pcal_print\",\n \"named\": true\n },\n {\n \"type\": \"pcal_proc_call\",\n \"named\": true\n },\n {\n \"type\": \"pcal_return\",\n \"named\": true\n },\n {\n \"type\": \"pcal_skip\",\n \"named\": true\n },\n {\n \"type\": \"pcal_while\",\n \"named\": true\n },\n {\n \"type\": \"pcal_with\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"pcal_algorithm_start\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": false,\n \"required\": false,\n \"types\": [\n {\n \"type\": \"fair\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"pcal_assert\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"pcal_assign\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n },\n {\n \"type\": \"assign\",\n \"named\": true\n },\n {\n \"type\": \"pcal_lhs\",\n \"named\": true\n },\n {\n \"type\": \"vertvert\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"pcal_await\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"pcal_definitions\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"function_definition\",\n \"named\": true\n },\n {\n \"type\": \"instance\",\n \"named\": true\n },\n {\n \"type\": \"module_definition\",\n \"named\": true\n },\n {\n \"type\": \"operator_definition\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"pcal_either\",\n \"named\": true,\n \"fields\": {\n \"label\": {\n \"multiple\": true,\n \"required\": false,\n \"types\": [\n {\n \"type\": \":\",\n \"named\": false\n },\n {\n \"type\": \"identifier\",\n \"named\": true\n }\n ]\n }\n },\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"pcal_algorithm_body\",\n \"named\": true\n },\n {\n \"type\": \"pcal_assert\",\n \"named\": true\n },\n {\n \"type\": \"pcal_assign\",\n \"named\": true\n },\n {\n \"type\": \"pcal_await\",\n \"named\": true\n },\n {\n \"type\": \"pcal_either\",\n \"named\": true\n },\n {\n \"type\": \"pcal_end_either\",\n \"named\": true\n },\n {\n \"type\": \"pcal_goto\",\n \"named\": true\n },\n {\n \"type\": \"pcal_if\",\n \"named\": true\n },\n {\n \"type\": \"pcal_macro_call\",\n \"named\": true\n },\n {\n \"type\": \"pcal_print\",\n \"named\": true\n },\n {\n \"type\": \"pcal_proc_call\",\n \"named\": true\n },\n {\n \"type\": \"pcal_return\",\n \"named\": true\n },\n {\n \"type\": \"pcal_skip\",\n \"named\": true\n },\n {\n \"type\": \"pcal_while\",\n \"named\": true\n },\n {\n \"type\": \"pcal_with\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"pcal_goto\",\n \"named\": true,\n \"fields\": {\n \"statement\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"identifier\",\n \"named\": true\n }\n ]\n }\n }\n },\n {\n \"type\": \"pcal_if\",\n \"named\": true,\n \"fields\": {\n \"label\": {\n \"multiple\": true,\n \"required\": false,\n \"types\": [\n {\n \"type\": \":\",\n \"named\": false\n },\n {\n \"type\": \"identifier\",\n \"named\": true\n }\n ]\n }\n },\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n },\n {\n \"type\": \"pcal_algorithm_body\",\n \"named\": true\n },\n {\n \"type\": \"pcal_assert\",\n \"named\": true\n },\n {\n \"type\": \"pcal_assign\",\n \"named\": true\n },\n {\n \"type\": \"pcal_await\",\n \"named\": true\n },\n {\n \"type\": \"pcal_either\",\n \"named\": true\n },\n {\n \"type\": \"pcal_end_if\",\n \"named\": true\n },\n {\n \"type\": \"pcal_goto\",\n \"named\": true\n },\n {\n \"type\": \"pcal_if\",\n \"named\": true\n },\n {\n \"type\": \"pcal_macro_call\",\n \"named\": true\n },\n {\n \"type\": \"pcal_print\",\n \"named\": true\n },\n {\n \"type\": \"pcal_proc_call\",\n \"named\": true\n },\n {\n \"type\": \"pcal_return\",\n \"named\": true\n },\n {\n \"type\": \"pcal_skip\",\n \"named\": true\n },\n {\n \"type\": \"pcal_while\",\n \"named\": true\n },\n {\n \"type\": \"pcal_with\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"pcal_lhs\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n },\n {\n \"type\": \"identifier\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"pcal_macro\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"pcal_algorithm_body\",\n \"named\": true\n },\n {\n \"type\": \"pcal_macro_decl\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"pcal_macro_call\",\n \"named\": true,\n \"fields\": {\n \"name\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"identifier\",\n \"named\": true\n }\n ]\n }\n },\n \"children\": {\n \"multiple\": true,\n \"required\": false,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"pcal_macro_decl\",\n \"named\": true,\n \"fields\": {\n \"name\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"identifier\",\n \"named\": true\n }\n ]\n },\n \"parameter\": {\n \"multiple\": true,\n \"required\": false,\n \"types\": [\n {\n \"type\": \"identifier\",\n \"named\": true\n }\n ]\n }\n }\n },\n {\n \"type\": \"pcal_print\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"pcal_proc_call\",\n \"named\": true,\n \"fields\": {\n \"name\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"identifier\",\n \"named\": true\n }\n ]\n }\n },\n \"children\": {\n \"multiple\": true,\n \"required\": false,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"pcal_proc_decl\",\n \"named\": true,\n \"fields\": {\n \"name\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"identifier\",\n \"named\": true\n }\n ]\n }\n },\n \"children\": {\n \"multiple\": true,\n \"required\": false,\n \"types\": [\n {\n \"type\": \"pcal_proc_var_decl\",\n \"named\": true\n },\n {\n \"type\": \"pcal_proc_var_decls\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"pcal_proc_var_decl\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n },\n {\n \"type\": \"identifier\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"pcal_proc_var_decls\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"pcal_proc_var_decl\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"pcal_procedure\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"pcal_algorithm_body\",\n \"named\": true\n },\n {\n \"type\": \"pcal_proc_decl\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"pcal_process\",\n \"named\": true,\n \"fields\": {\n \"name\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"identifier\",\n \"named\": true\n }\n ]\n }\n },\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n },\n {\n \"type\": \"pcal_algorithm_body\",\n \"named\": true\n },\n {\n \"type\": \"pcal_var_decls\",\n \"named\": true\n },\n {\n \"type\": \"set_in\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"pcal_return\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"pcal_skip\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"pcal_var_decl\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n },\n {\n \"type\": \"identifier\",\n \"named\": true\n },\n {\n \"type\": \"set_in\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"pcal_var_decls\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"pcal_var_decl\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"pcal_while\",\n \"named\": true,\n \"fields\": {\n \"label\": {\n \"multiple\": true,\n \"required\": false,\n \"types\": [\n {\n \"type\": \":\",\n \"named\": false\n },\n {\n \"type\": \"identifier\",\n \"named\": true\n }\n ]\n }\n },\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n },\n {\n \"type\": \"pcal_algorithm_body\",\n \"named\": true\n },\n {\n \"type\": \"pcal_assert\",\n \"named\": true\n },\n {\n \"type\": \"pcal_assign\",\n \"named\": true\n },\n {\n \"type\": \"pcal_await\",\n \"named\": true\n },\n {\n \"type\": \"pcal_either\",\n \"named\": true\n },\n {\n \"type\": \"pcal_end_while\",\n \"named\": true\n },\n {\n \"type\": \"pcal_goto\",\n \"named\": true\n },\n {\n \"type\": \"pcal_if\",\n \"named\": true\n },\n {\n \"type\": \"pcal_macro_call\",\n \"named\": true\n },\n {\n \"type\": \"pcal_print\",\n \"named\": true\n },\n {\n \"type\": \"pcal_proc_call\",\n \"named\": true\n },\n {\n \"type\": \"pcal_return\",\n \"named\": true\n },\n {\n \"type\": \"pcal_skip\",\n \"named\": true\n },\n {\n \"type\": \"pcal_while\",\n \"named\": true\n },\n {\n \"type\": \"pcal_with\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"pcal_with\",\n \"named\": true,\n \"fields\": {\n \"label\": {\n \"multiple\": true,\n \"required\": false,\n \"types\": [\n {\n \"type\": \":\",\n \"named\": false\n },\n {\n \"type\": \"identifier\",\n \"named\": true\n }\n ]\n }\n },\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n },\n {\n \"type\": \"identifier\",\n \"named\": true\n },\n {\n \"type\": \"pcal_algorithm_body\",\n \"named\": true\n },\n {\n \"type\": \"pcal_assert\",\n \"named\": true\n },\n {\n \"type\": \"pcal_assign\",\n \"named\": true\n },\n {\n \"type\": \"pcal_await\",\n \"named\": true\n },\n {\n \"type\": \"pcal_either\",\n \"named\": true\n },\n {\n \"type\": \"pcal_end_with\",\n \"named\": true\n },\n {\n \"type\": \"pcal_goto\",\n \"named\": true\n },\n {\n \"type\": \"pcal_if\",\n \"named\": true\n },\n {\n \"type\": \"pcal_macro_call\",\n \"named\": true\n },\n {\n \"type\": \"pcal_print\",\n \"named\": true\n },\n {\n \"type\": \"pcal_proc_call\",\n \"named\": true\n },\n {\n \"type\": \"pcal_return\",\n \"named\": true\n },\n {\n \"type\": \"pcal_skip\",\n \"named\": true\n },\n {\n \"type\": \"pcal_while\",\n \"named\": true\n },\n {\n \"type\": \"pcal_with\",\n \"named\": true\n },\n {\n \"type\": \"set_in\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"pick_proof_step\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n },\n {\n \"type\": \"_proof\",\n \"named\": true\n },\n {\n \"type\": \"identifier\",\n \"named\": true\n },\n {\n \"type\": \"quantifier_bound\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"plus\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"plus_arrow\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"postfix_op_symbol\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"asterisk\",\n \"named\": true\n },\n {\n \"type\": \"prime\",\n \"named\": true\n },\n {\n \"type\": \"sup_hash\",\n \"named\": true\n },\n {\n \"type\": \"sup_plus\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"powerset\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"prec\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"preceq\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"prefix_op_symbol\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"always\",\n \"named\": true\n },\n {\n \"type\": \"domain\",\n \"named\": true\n },\n {\n \"type\": \"enabled\",\n \"named\": true\n },\n {\n \"type\": \"eventually\",\n \"named\": true\n },\n {\n \"type\": \"lnot\",\n \"named\": true\n },\n {\n \"type\": \"negative\",\n \"named\": true\n },\n {\n \"type\": \"powerset\",\n \"named\": true\n },\n {\n \"type\": \"unchanged\",\n \"named\": true\n },\n {\n \"type\": \"union\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"prefixed_op\",\n \"named\": true,\n \"fields\": {\n \"op\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"bound_nonfix_op\",\n \"named\": true\n },\n {\n \"type\": \"bound_op\",\n \"named\": true\n },\n {\n \"type\": \"identifier_ref\",\n \"named\": true\n }\n ]\n },\n \"prefix\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"subexpr_prefix\",\n \"named\": true\n }\n ]\n }\n }\n },\n {\n \"type\": \"prev_func_val\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"proof_step\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"case_proof_step\",\n \"named\": true\n },\n {\n \"type\": \"definition_proof_step\",\n \"named\": true\n },\n {\n \"type\": \"have_proof_step\",\n \"named\": true\n },\n {\n \"type\": \"instance\",\n \"named\": true\n },\n {\n \"type\": \"pick_proof_step\",\n \"named\": true\n },\n {\n \"type\": \"proof_step_id\",\n \"named\": true\n },\n {\n \"type\": \"suffices_proof_step\",\n \"named\": true\n },\n {\n \"type\": \"take_proof_step\",\n \"named\": true\n },\n {\n \"type\": \"use_or_hide\",\n \"named\": true\n },\n {\n \"type\": \"witness_proof_step\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"proof_step_id\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"level\",\n \"named\": true\n },\n {\n \"type\": \"name\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"proof_step_ref\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"level\",\n \"named\": true\n },\n {\n \"type\": \"name\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"propto\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"qed_step\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_proof\",\n \"named\": true\n },\n {\n \"type\": \"proof_step_id\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"qq\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"quantifier_bound\",\n \"named\": true,\n \"fields\": {\n \"intro\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \",\",\n \"named\": false\n },\n {\n \"type\": \"identifier\",\n \"named\": true\n },\n {\n \"type\": \"tuple_of_identifiers\",\n \"named\": true\n }\n ]\n },\n \"set\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n }\n },\n \"children\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"set_in\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"rangle_bracket\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"rangle_bracket_sub\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"rd_ttile\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"real_number_set\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"record_literal\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n },\n {\n \"type\": \"all_map_to\",\n \"named\": true\n },\n {\n \"type\": \"identifier\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"record_value\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"recursive_declaration\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"identifier\",\n \"named\": true\n },\n {\n \"type\": \"operator_declaration\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"rs_ttile\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"set_filter\",\n \"named\": true,\n \"fields\": {\n \"filter\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n },\n \"generator\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"quantifier_bound\",\n \"named\": true\n }\n ]\n }\n }\n },\n {\n \"type\": \"set_in\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"set_map\",\n \"named\": true,\n \"fields\": {\n \"generator\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \",\",\n \"named\": false\n },\n {\n \"type\": \"quantifier_bound\",\n \"named\": true\n }\n ]\n },\n \"map\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n }\n }\n },\n {\n \"type\": \"set_of_functions\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n },\n {\n \"type\": \"maps_to\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"set_of_records\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n },\n {\n \"type\": \"identifier\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"sim\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"simeq\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"single_line\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"source_file\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": false,\n \"types\": [\n {\n \"type\": \"_unit\",\n \"named\": true\n },\n {\n \"type\": \"extends\",\n \"named\": true\n },\n {\n \"type\": \"extramodular_text\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"sqcap\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"sqcup\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"sqsubset\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"sqsubseteq\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"sqsupset\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"sqsupseteq\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"star\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"statement_level\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"step_expr_no_stutter\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n },\n {\n \"type\": \"langle_bracket\",\n \"named\": true\n },\n {\n \"type\": \"rangle_bracket_sub\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"step_expr_or_stutter\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"string\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": false,\n \"types\": [\n {\n \"type\": \"escape_char\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"subexpr_component\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"bound_nonfix_op\",\n \"named\": true\n },\n {\n \"type\": \"bound_op\",\n \"named\": true\n },\n {\n \"type\": \"identifier_ref\",\n \"named\": true\n },\n {\n \"type\": \"infix_op_symbol\",\n \"named\": true\n },\n {\n \"type\": \"postfix_op_symbol\",\n \"named\": true\n },\n {\n \"type\": \"prefix_op_symbol\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"subexpr_prefix\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"proof_step_ref\",\n \"named\": true\n },\n {\n \"type\": \"subexpr_component\",\n \"named\": true\n },\n {\n \"type\": \"subexpr_tree_nav\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"subexpr_tree_nav\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"address\",\n \"named\": true\n },\n {\n \"type\": \"child_id\",\n \"named\": true\n },\n {\n \"type\": \"colon\",\n \"named\": true\n },\n {\n \"type\": \"langle_bracket\",\n \"named\": true\n },\n {\n \"type\": \"operator_args\",\n \"named\": true\n },\n {\n \"type\": \"rangle_bracket\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"subexpression\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"subexpr_prefix\",\n \"named\": true\n },\n {\n \"type\": \"subexpr_tree_nav\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"subset\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"subseteq\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"substitution\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n },\n {\n \"type\": \"_op\",\n \"named\": true\n },\n {\n \"type\": \"gets\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"succ\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"succeq\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"suffices_proof_step\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n },\n {\n \"type\": \"_proof\",\n \"named\": true\n },\n {\n \"type\": \"assume_prove\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"sup_plus\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"supset\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"supseteq\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"take_proof_step\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"identifier\",\n \"named\": true\n },\n {\n \"type\": \"quantifier_bound\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"temporal_exists\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"temporal_forall\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"terminal_proof\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": false,\n \"required\": false,\n \"types\": [\n {\n \"type\": \"use_body\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"theorem\",\n \"named\": true,\n \"fields\": {\n \"name\": {\n \"multiple\": false,\n \"required\": false,\n \"types\": [\n {\n \"type\": \"identifier\",\n \"named\": true\n }\n ]\n },\n \"proof\": {\n \"multiple\": false,\n \"required\": false,\n \"types\": [\n {\n \"type\": \"_proof\",\n \"named\": true\n }\n ]\n },\n \"statement\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n },\n {\n \"type\": \"assume_prove\",\n \"named\": true\n }\n ]\n }\n },\n \"children\": {\n \"multiple\": false,\n \"required\": false,\n \"types\": [\n {\n \"type\": \"def_eq\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"times\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"tuple_literal\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n },\n {\n \"type\": \"langle_bracket\",\n \"named\": true\n },\n {\n \"type\": \"rangle_bracket\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"tuple_of_identifiers\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"identifier\",\n \"named\": true\n },\n {\n \"type\": \"langle_bracket\",\n \"named\": true\n },\n {\n \"type\": \"rangle_bracket\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"unbounded_quantification\",\n \"named\": true,\n \"fields\": {\n \"expression\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n },\n \"intro\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \",\",\n \"named\": false\n },\n {\n \"type\": \"identifier\",\n \"named\": true\n }\n ]\n },\n \"quantifier\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"exists\",\n \"named\": true\n },\n {\n \"type\": \"forall\",\n \"named\": true\n },\n {\n \"type\": \"temporal_exists\",\n \"named\": true\n },\n {\n \"type\": \"temporal_forall\",\n \"named\": true\n }\n ]\n }\n }\n },\n {\n \"type\": \"unchanged\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"union\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"uplus\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"use_body\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"use_body_def\",\n \"named\": true\n },\n {\n \"type\": \"use_body_expr\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"use_body_def\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n },\n {\n \"type\": \"_op\",\n \"named\": true\n },\n {\n \"type\": \"module_ref\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"use_body_expr\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n },\n {\n \"type\": \"module_ref\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"use_or_hide\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": false,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"use_body\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"variable_declaration\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"identifier\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"vertvert\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"witness_proof_step\",\n \"named\": true,\n \"fields\": {},\n \"children\": {\n \"multiple\": true,\n \"required\": true,\n \"types\": [\n {\n \"type\": \"_expr\",\n \"named\": true\n }\n ]\n }\n },\n {\n \"type\": \"wr\",\n \"named\": true,\n \"fields\": {}\n },\n {\n \"type\": \"!\",\n \"named\": false\n },\n {\n \"type\": \"!!\",\n \"named\": false\n },\n {\n \"type\": \"\\\"\",\n \"named\": false\n },\n {\n \"type\": \"#\",\n \"named\": false\n },\n {\n \"type\": \"(\",\n \"named\": false\n },\n {\n \"type\": \"(*\",\n \"named\": false\n },\n {\n \"type\": \"(+)\",\n \"named\": false\n },\n {\n \"type\": \"(-)\",\n \"named\": false\n },\n {\n \"type\": \"(.)\",\n \"named\": false\n },\n {\n \"type\": \"(/)\",\n \"named\": false\n },\n {\n \"type\": \"(\\\\X)\",\n \"named\": false\n },\n {\n \"type\": \")\",\n \"named\": false\n },\n {\n \"type\": \"*)\",\n \"named\": false\n },\n {\n \"type\": \"+\",\n \"named\": false\n },\n {\n \"type\": \",\",\n \"named\": false\n },\n {\n \"type\": \"-\",\n \"named\": false\n },\n {\n \"type\": \"-+->\",\n \"named\": false\n },\n {\n \"type\": \"----\",\n \"named\": false\n },\n {\n \"type\": \"--algorithm\",\n \"named\": false\n },\n {\n \"type\": \"--fair\",\n \"named\": false\n },\n {\n \"type\": \"->\",\n \"named\": false\n },\n {\n \"type\": \"-|\",\n \"named\": false\n },\n {\n \"type\": \".\",\n \"named\": false\n },\n {\n \"type\": \"..\",\n \"named\": false\n },\n {\n \"type\": \"...\",\n \"named\": false\n },\n {\n \"type\": \"/=\",\n \"named\": false\n },\n {\n \"type\": \"/\\\\\",\n \"named\": false\n },\n {\n \"type\": \":\",\n \"named\": false\n },\n {\n \"type\": \"::\",\n \"named\": false\n },\n {\n \"type\": \"::=\",\n \"named\": false\n },\n {\n \"type\": \":=\",\n \"named\": false\n },\n {\n \"type\": \";\",\n \"named\": false\n },\n {\n \"type\": \"<\",\n \"named\": false\n },\n {\n \"type\": \"<-\",\n \"named\": false\n },\n {\n \"type\": \"<<\",\n \"named\": false\n },\n {\n \"type\": \"<=\",\n \"named\": false\n },\n {\n \"type\": \"<=>\",\n \"named\": false\n },\n {\n \"type\": \"<>\",\n \"named\": false\n },\n {\n \"type\": \"=\",\n \"named\": false\n },\n {\n \"type\": \"=<\",\n \"named\": false\n },\n {\n \"type\": \"==\",\n \"named\": false\n },\n {\n \"type\": \"====\",\n \"named\": false\n },\n {\n \"type\": \"=>\",\n \"named\": false\n },\n {\n \"type\": \"=|\",\n \"named\": false\n },\n {\n \"type\": \">\",\n \"named\": false\n },\n {\n \"type\": \">=\",\n \"named\": false\n },\n {\n \"type\": \">>\",\n \"named\": false\n },\n {\n \"type\": \">>_\",\n \"named\": false\n },\n {\n \"type\": \"??\",\n \"named\": false\n },\n {\n \"type\": \"@\",\n \"named\": false\n },\n {\n \"type\": \"ACTION\",\n \"named\": false\n },\n {\n \"type\": \"ASSUME\",\n \"named\": false\n },\n {\n \"type\": \"ASSUMPTION\",\n \"named\": false\n },\n {\n \"type\": \"AXIOM\",\n \"named\": false\n },\n {\n \"type\": \"BY\",\n \"named\": false\n },\n {\n \"type\": \"CASE\",\n \"named\": false\n },\n {\n \"type\": \"CHOOSE\",\n \"named\": false\n },\n {\n \"type\": \"CONSTANT\",\n \"named\": false\n },\n {\n \"type\": \"CONSTANTS\",\n \"named\": false\n },\n {\n \"type\": \"COROLLARY\",\n \"named\": false\n },\n {\n \"type\": \"DEF\",\n \"named\": false\n },\n {\n \"type\": \"DEFINE\",\n \"named\": false\n },\n {\n \"type\": \"DEFS\",\n \"named\": false\n },\n {\n \"type\": \"DOMAIN\",\n \"named\": false\n },\n {\n \"type\": \"ELSE\",\n \"named\": false\n },\n {\n \"type\": \"ENABLED\",\n \"named\": false\n },\n {\n \"type\": \"EXCEPT\",\n \"named\": false\n },\n {\n \"type\": \"EXTENDS\",\n \"named\": false\n },\n {\n \"type\": \"FALSE\",\n \"named\": false\n },\n {\n \"type\": \"HAVE\",\n \"named\": false\n },\n {\n \"type\": \"HIDE\",\n \"named\": false\n },\n {\n \"type\": \"IF\",\n \"named\": false\n },\n {\n \"type\": \"IN\",\n \"named\": false\n },\n {\n \"type\": \"INSTANCE\",\n \"named\": false\n },\n {\n \"type\": \"Int\",\n \"named\": false\n },\n {\n \"type\": \"LAMBDA\",\n \"named\": false\n },\n {\n \"type\": \"LEMMA\",\n \"named\": false\n },\n {\n \"type\": \"LET\",\n \"named\": false\n },\n {\n \"type\": \"LOCAL\",\n \"named\": false\n },\n {\n \"type\": \"MODULE\",\n \"named\": false\n },\n {\n \"type\": \"NEW\",\n \"named\": false\n },\n {\n \"type\": \"Nat\",\n \"named\": false\n },\n {\n \"type\": \"OBVIOUS\",\n \"named\": false\n },\n {\n \"type\": \"OMITTED\",\n \"named\": false\n },\n {\n \"type\": \"ONLY\",\n \"named\": false\n },\n {\n \"type\": \"OTHER\",\n \"named\": false\n },\n {\n \"type\": \"PICK\",\n \"named\": false\n },\n {\n \"type\": \"PROOF\",\n \"named\": false\n },\n {\n \"type\": \"PROPOSITION\",\n \"named\": false\n },\n {\n \"type\": \"PROVE\",\n \"named\": false\n },\n {\n \"type\": \"QED\",\n \"named\": false\n },\n {\n \"type\": \"RECURSIVE\",\n \"named\": false\n },\n {\n \"type\": \"Real\",\n \"named\": false\n },\n {\n \"type\": \"SF_\",\n \"named\": false\n },\n {\n \"type\": \"STATE\",\n \"named\": false\n },\n {\n \"type\": \"SUBSET\",\n \"named\": false\n },\n {\n \"type\": \"SUFFICES\",\n \"named\": false\n },\n {\n \"type\": \"TAKE\",\n \"named\": false\n },\n {\n \"type\": \"TEMPORAL\",\n \"named\": false\n },\n {\n \"type\": \"THEN\",\n \"named\": false\n },\n {\n \"type\": \"THEOREM\",\n \"named\": false\n },\n {\n \"type\": \"TRUE\",\n \"named\": false\n },\n {\n \"type\": \"UNCHANGED\",\n \"named\": false\n },\n {\n \"type\": \"UNION\",\n \"named\": false\n },\n {\n \"type\": \"USE\",\n \"named\": false\n },\n {\n \"type\": \"VARIABLE\",\n \"named\": false\n },\n {\n \"type\": \"VARIABLES\",\n \"named\": false\n },\n {\n \"type\": \"WF_\",\n \"named\": false\n },\n {\n \"type\": \"WITH\",\n \"named\": false\n },\n {\n \"type\": \"WITNESS\",\n \"named\": false\n },\n {\n \"type\": \"[\",\n \"named\": false\n },\n {\n \"type\": \"[]\",\n \"named\": false\n },\n {\n \"type\": \"\\\\/\",\n \"named\": false\n },\n {\n \"type\": \"\\\\A\",\n \"named\": false\n },\n {\n \"type\": \"\\\\AA\",\n \"named\": false\n },\n {\n \"type\": \"\\\\E\",\n \"named\": false\n },\n {\n \"type\": \"\\\\EE\",\n \"named\": false\n },\n {\n \"type\": \"\\\\X\",\n \"named\": false\n },\n {\n \"type\": \"\\\\approx\",\n \"named\": false\n },\n {\n \"type\": \"\\\\asymp\",\n \"named\": false\n },\n {\n \"type\": \"\\\\bigcirc\",\n \"named\": false\n },\n {\n \"type\": \"\\\\bullet\",\n \"named\": false\n },\n {\n \"type\": \"\\\\cap\",\n \"named\": false\n },\n {\n \"type\": \"\\\\cdot\",\n \"named\": false\n },\n {\n \"type\": \"\\\\circ\",\n \"named\": false\n },\n {\n \"type\": \"\\\\cong\",\n \"named\": false\n },\n {\n \"type\": \"\\\\cup\",\n \"named\": false\n },\n {\n \"type\": \"\\\\div\",\n \"named\": false\n },\n {\n \"type\": \"\\\\doteq\",\n \"named\": false\n },\n {\n \"type\": \"\\\\equiv\",\n \"named\": false\n },\n {\n \"type\": \"\\\\exists\",\n \"named\": false\n },\n {\n \"type\": \"\\\\forall\",\n \"named\": false\n },\n {\n \"type\": \"\\\\geq\",\n \"named\": false\n },\n {\n \"type\": \"\\\\gg\",\n \"named\": false\n },\n {\n \"type\": \"\\\\in\",\n \"named\": false\n },\n {\n \"type\": \"\\\\intersect\",\n \"named\": false\n },\n {\n \"type\": \"\\\\land\",\n \"named\": false\n },\n {\n \"type\": \"\\\\leq\",\n \"named\": false\n },\n {\n \"type\": \"\\\\ll\",\n \"named\": false\n },\n {\n \"type\": \"\\\\lnot\",\n \"named\": false\n },\n {\n \"type\": \"\\\\lor\",\n \"named\": false\n },\n {\n \"type\": \"\\\\neg\",\n \"named\": false\n },\n {\n \"type\": \"\\\\notin\",\n \"named\": false\n },\n {\n \"type\": \"\\\\o\",\n \"named\": false\n },\n {\n \"type\": \"\\\\odot\",\n \"named\": false\n },\n {\n \"type\": \"\\\\ominus\",\n \"named\": false\n },\n {\n \"type\": \"\\\\oplus\",\n \"named\": false\n },\n {\n \"type\": \"\\\\oslash\",\n \"named\": false\n },\n {\n \"type\": \"\\\\otimes\",\n \"named\": false\n },\n {\n \"type\": \"\\\\prec\",\n \"named\": false\n },\n {\n \"type\": \"\\\\preceq\",\n \"named\": false\n },\n {\n \"type\": \"\\\\propto\",\n \"named\": false\n },\n {\n \"type\": \"\\\\sim\",\n \"named\": false\n },\n {\n \"type\": \"\\\\simeq\",\n \"named\": false\n },\n {\n \"type\": \"\\\\sqcap\",\n \"named\": false\n },\n {\n \"type\": \"\\\\sqcup\",\n \"named\": false\n },\n {\n \"type\": \"\\\\sqsubset\",\n \"named\": false\n },\n {\n \"type\": \"\\\\sqsubseteq\",\n \"named\": false\n },\n {\n \"type\": \"\\\\sqsupset\",\n \"named\": false\n },\n {\n \"type\": \"\\\\sqsupseteq\",\n \"named\": false\n },\n {\n \"type\": \"\\\\star\",\n \"named\": false\n },\n {\n \"type\": \"\\\\subset\",\n \"named\": false\n },\n {\n \"type\": \"\\\\subseteq\",\n \"named\": false\n },\n {\n \"type\": \"\\\\succ\",\n \"named\": false\n },\n {\n \"type\": \"\\\\succeq\",\n \"named\": false\n },\n {\n \"type\": \"\\\\supset\",\n \"named\": false\n },\n {\n \"type\": \"\\\\supseteq\",\n \"named\": false\n },\n {\n \"type\": \"\\\\times\",\n \"named\": false\n },\n {\n \"type\": \"\\\\union\",\n \"named\": false\n },\n {\n \"type\": \"\\\\uplus\",\n \"named\": false\n },\n {\n \"type\": \"\\\\wr\",\n \"named\": false\n },\n {\n \"type\": \"]\",\n \"named\": false\n },\n {\n \"type\": \"]_\",\n \"named\": false\n },\n {\n \"type\": \"^+\",\n \"named\": false\n },\n {\n \"type\": \"algorithm\",\n \"named\": false\n },\n {\n \"type\": \"amp\",\n \"named\": true\n },\n {\n \"type\": \"ampamp\",\n \"named\": true\n },\n {\n \"type\": \"assert\",\n \"named\": false\n },\n {\n \"type\": \"asterisk\",\n \"named\": true\n },\n {\n \"type\": \"await\",\n \"named\": false\n },\n {\n \"type\": \"begin\",\n \"named\": false\n },\n {\n \"type\": \"boolean_set\",\n \"named\": true\n },\n {\n \"type\": \"call\",\n \"named\": false\n },\n {\n \"type\": \"comment\",\n \"named\": true\n },\n {\n \"type\": \"compose\",\n \"named\": true\n },\n {\n \"type\": \"define\",\n \"named\": false\n },\n {\n \"type\": \"do\",\n \"named\": false\n },\n {\n \"type\": \"dol\",\n \"named\": true\n },\n {\n \"type\": \"doldol\",\n \"named\": true\n },\n {\n \"type\": \"either\",\n \"named\": false\n },\n {\n \"type\": \"else\",\n \"named\": false\n },\n {\n \"type\": \"elsif\",\n \"named\": false\n },\n {\n \"type\": \"end\",\n \"named\": false\n },\n {\n \"type\": \"escape_char\",\n \"named\": true\n },\n {\n \"type\": \"extramodular_text\",\n \"named\": true\n },\n {\n \"type\": \"fair\",\n \"named\": false\n },\n {\n \"type\": \"format\",\n \"named\": true\n },\n {\n \"type\": \"goto\",\n \"named\": false\n },\n {\n \"type\": \"gt\",\n \"named\": true\n },\n {\n \"type\": \"hashhash\",\n \"named\": true\n },\n {\n \"type\": \"identifier\",\n \"named\": true\n },\n {\n \"type\": \"identifier_ref\",\n \"named\": true\n },\n {\n \"type\": \"if\",\n \"named\": false\n },\n {\n \"type\": \"level\",\n \"named\": true\n },\n {\n \"type\": \"macro\",\n \"named\": false\n },\n {\n \"type\": \"map_from\",\n \"named\": true\n },\n {\n \"type\": \"map_to\",\n \"named\": true\n },\n {\n \"type\": \"minusminus\",\n \"named\": true\n },\n {\n \"type\": \"mod\",\n \"named\": true\n },\n {\n \"type\": \"modmod\",\n \"named\": true\n },\n {\n \"type\": \"mul\",\n \"named\": true\n },\n {\n \"type\": \"mulmul\",\n \"named\": true\n },\n {\n \"type\": \"name\",\n \"named\": true\n },\n {\n \"type\": \"or\",\n \"named\": false\n },\n {\n \"type\": \"pcal_end_either\",\n \"named\": true\n },\n {\n \"type\": \"pcal_end_if\",\n \"named\": true\n },\n {\n \"type\": \"pcal_end_while\",\n \"named\": true\n },\n {\n \"type\": \"pcal_end_with\",\n \"named\": true\n },\n {\n \"type\": \"placeholder\",\n \"named\": true\n },\n {\n \"type\": \"plusplus\",\n \"named\": true\n },\n {\n \"type\": \"pow\",\n \"named\": true\n },\n {\n \"type\": \"powpow\",\n \"named\": true\n },\n {\n \"type\": \"prime\",\n \"named\": true\n },\n {\n \"type\": \"print\",\n \"named\": false\n },\n {\n \"type\": \"procedure\",\n \"named\": false\n },\n {\n \"type\": \"process\",\n \"named\": false\n },\n {\n \"type\": \"real_number\",\n \"named\": true\n },\n {\n \"type\": \"return\",\n \"named\": false\n },\n {\n \"type\": \"setminus\",\n \"named\": true\n },\n {\n \"type\": \"skip\",\n \"named\": false\n },\n {\n \"type\": \"slash\",\n \"named\": true\n },\n {\n \"type\": \"slashslash\",\n \"named\": true\n },\n {\n \"type\": \"string_set\",\n \"named\": true\n },\n {\n \"type\": \"sup_hash\",\n \"named\": true\n },\n {\n \"type\": \"then\",\n \"named\": false\n },\n {\n \"type\": \"value\",\n \"named\": true\n },\n {\n \"type\": \"variable\",\n \"named\": false\n },\n {\n \"type\": \"variables\",\n \"named\": false\n },\n {\n \"type\": \"vert\",\n \"named\": true\n },\n {\n \"type\": \"when\",\n \"named\": false\n },\n {\n \"type\": \"while\",\n \"named\": false\n },\n {\n \"type\": \"with\",\n \"named\": false\n },\n {\n \"type\": \"{\",\n \"named\": false\n },\n {\n \"type\": \"|-\",\n \"named\": false\n },\n {\n \"type\": \"|->\",\n \"named\": false\n },\n {\n \"type\": \"|=\",\n \"named\": false\n },\n {\n \"type\": \"||\",\n \"named\": false\n },\n {\n \"type\": \"}\",\n \"named\": false\n },\n {\n \"type\": \"~\",\n \"named\": false\n },\n {\n \"type\": \"~>\",\n \"named\": false\n },\n {\n \"type\": \"\u{ac}\",\n \"named\": false\n },\n {\n \"type\": \"\u{d7}\",\n \"named\": false\n },\n {\n \"type\": \"\u{f7}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2016}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2025}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2026}\",\n \"named\": false\n },\n {\n \"type\": \"\u{203c}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2047}\",\n \"named\": false\n },\n {\n \"type\": \"\u{207a}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2115}\",\n \"named\": false\n },\n {\n \"type\": \"\u{211d}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2124}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2190}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2192}\",\n \"named\": false\n },\n {\n \"type\": \"\u{219d}\",\n \"named\": false\n },\n {\n \"type\": \"\u{21a6}\",\n \"named\": false\n },\n {\n \"type\": \"\u{21d2}\",\n \"named\": false\n },\n {\n \"type\": \"\u{21d4}\",\n \"named\": false\n },\n {\n \"type\": \"\u{21dd}\",\n \"named\": false\n },\n {\n \"type\": \"\u{21f8}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2200}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2203}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2208}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2209}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2218}\",\n \"named\": false\n },\n {\n \"type\": \"\u{221d}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2227}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2228}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2229}\",\n \"named\": false\n },\n {\n \"type\": \"\u{222a}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2237}\",\n \"named\": false\n },\n {\n \"type\": \"\u{223c}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2240}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2243}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2245}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2248}\",\n \"named\": false\n },\n {\n \"type\": \"\u{224d}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2250}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2254}\",\n \"named\": false\n },\n {\n \"type\": \"\u{225c}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2260}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2261}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2264}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2265}\",\n \"named\": false\n },\n {\n \"type\": \"\u{226a}\",\n \"named\": false\n },\n {\n \"type\": \"\u{226b}\",\n \"named\": false\n },\n {\n \"type\": \"\u{227a}\",\n \"named\": false\n },\n {\n \"type\": \"\u{227b}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2282}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2283}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2286}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2287}\",\n \"named\": false\n },\n {\n \"type\": \"\u{228e}\",\n \"named\": false\n },\n {\n \"type\": \"\u{228f}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2290}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2291}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2292}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2293}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2294}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2295}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2296}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2297}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2298}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2299}\",\n \"named\": false\n },\n {\n \"type\": \"\u{22a2}\",\n \"named\": false\n },\n {\n \"type\": \"\u{22a3}\",\n \"named\": false\n },\n {\n \"type\": \"\u{22a8}\",\n \"named\": false\n },\n {\n \"type\": \"\u{22c4}\",\n \"named\": false\n },\n {\n \"type\": \"\u{22c5}\",\n \"named\": false\n },\n {\n \"type\": \"\u{22c6}\",\n \"named\": false\n },\n {\n \"type\": \"\u{25a1}\",\n \"named\": false\n },\n {\n \"type\": \"\u{25c7}\",\n \"named\": false\n },\n {\n \"type\": \"\u{25cf}\",\n \"named\": false\n },\n {\n \"type\": \"\u{25ef}\",\n \"named\": false\n },\n {\n \"type\": \"\u{27e8}\",\n \"named\": false\n },\n {\n \"type\": \"\u{27e9}\",\n \"named\": false\n },\n {\n \"type\": \"\u{27e9}_\",\n \"named\": false\n },\n {\n \"type\": \"\u{27f5}\",\n \"named\": false\n },\n {\n \"type\": \"\u{27f6}\",\n \"named\": false\n },\n {\n \"type\": \"\u{27f9}\",\n \"named\": false\n },\n {\n \"type\": \"\u{27fa}\",\n \"named\": false\n },\n {\n \"type\": \"\u{27fc}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2945}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2a74}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2aaf}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2ab0}\",\n \"named\": false\n },\n {\n \"type\": \"\u{2ae4}\",\n \"named\": false\n },\n {\n \"type\": \"\u{3008}\",\n \"named\": false\n },\n {\n \"type\": \"\u{3009}\",\n \"named\": false\n },\n {\n \"type\": \"\u{3009}_\",\n \"named\": false\n }\n]";Expand description
The content of the node-types.json file for this grammar.