Source file syntax_messages.ml

(* This file was auto-generated based on "syntax.messages". *)

(* Please note that the function [message] can raise [Not_found]. *)

let message =
  fun s ->
    match s with
    | 0 ->
        "116\nan input statement\nan opening parenthesis to start a command\n"
    | 1 ->
        "115\na command\na command name\n"
    | 2 ->
        "114\na set-option command\nan attribute of the form \"keyword value?\"\n"
    | 3 ->
        "158\nan attribute\neither an attribute value as s-expression,\nanother attribute, or a closing parenthesis\n"
    | 6 ->
        "157\nan attribute value\na closing parenthesis, or an s-expression, i.e.\na literal, symbol, keyword, or an s-expression in parentheses\n"
    | 15 ->
        "156\na list of s-expressions\na closing parenthesis, or another s-expression, i.e.\na literal, symbol, keyword, or an s-expression in parentheses\n"
    | 8 ->
        "155\nan s-expression\na literal, symbol, keyword, or another s-expression in parentheses\n"
    | 24 ->
        "113\na set-option command\na closing parenthesis, or an attribute value;\nnote that keywords and reserved words (such as '_', 'as', ...) are not\nvalid attribute values, and thus are not allowed here\n"
    | 27 ->
        "112\na set-logic command\na symbol for the logic name\n"
    | 28 ->
        "111\na set-logic command\na closing parenthesis\n"
    | 30 ->
        "110\na set-info command\nan attribute of the form \"keyword value?\"\n"
    | 31 ->
        "109\na set-info command\na closing parenthesis, or an attribute value;\nnote that keywords and reserved words (such as '_', 'as', ...) are not\nvalid attribute values, and thus are not allowed here\n"
    | 33 ->
        "108\na reset-assertions command\na closing parenthesis\n"
    | 285 ->
        "116\nan input statement\nan opening parenthesis to start a command\n"
    | 35 ->
        "107\na reset command\na closing parenthesis\n"
    | 37 ->
        "106\na push command\na numeral\n"
    | 38 ->
        "105\na push command\na closing parenthesis\n"
    | 40 ->
        "104\na pop command\na numeral\n"
    | 41 ->
        "103\na pop command\na closing parenthesis\n"
    | 43 ->
        "102\na get-value command\nan opening parenthesis to start a list of terms\n"
    | 44 ->
        "101\na get-value command\na term\n"
    | 134 ->
        "100\na get-value command\na closing parenthesis\n"
    | 136 ->
        "099\na get-unsat-core command\na closing parenthesis\n"
    | 138 ->
        "098\na get-unsat-assumptions command\na closing parenthesis\n"
    | 140 ->
        "097\na get-proof command\na closing parenthesis\n"
    | 142 ->
        "096\na get-option command\na keyword of the form \":symbol\"\n"
    | 143 ->
        "095\na get-option command\na closing parenthesis\n"
    | 145 ->
        "094\na get-model command\na closing parenthesis\n"
    | 147 ->
        "093\na get-info command\na keyword of the form \":symbol\"\n"
    | 149 ->
        "092\na get-info command\na closing parenthesis\n"
    | 151 ->
        "091\na get-assignment command\na closing parenthesis\n"
    | 153 ->
        "090\na get-assertions command\na closing parenthesis\n"
    | 155 ->
        "089\nan exit command\na closing parenthesis\n"
    | 157 ->
        "088\nan echo command\na string literal\n"
    | 158 ->
        "087\nan echo command\na closing parenthesis\n"
    | 160 ->
        "086\na sort definition\na symbol for the defined sort's name\n"
    | 161 ->
        "085\na sort definition\nan opening parenthesis to start a list of arguments\n"
    | 162 ->
        "084\na sort definition\na closing parenthesis, or a list of symbols for the definition arguments\n"
    | 163 ->
        "154\na list of symbols\nanother symbol or a closing parenthesis\n"
    | 166 ->
        "083\na sort definition\na sort for the definition body\n"
    | 167 ->
        "082\na sort definition\na closing parenthesis\n"
    | 169 ->
        "081\na recursive function definition\na symbol for the function's name\n"
    | 170 ->
        "153\na function definition\nan opening parenthesis to start the list of arguments\n"
    | 171 ->
        "152\na function definition\na sorted variable of the form \"(var sort)\", or a closing parenthesis\n"
    | 172 ->
        "151\na list of sorted variables\nanother sorted variable of the form \"(var sort)\", or a closing parenthesis\n"
    | 175 ->
        "150\na function definition\na sort for the return type of the function\n"
    | 176 ->
        "149\na function definition\na term for the body of the function\n"
    | 178 ->
        "080\na recursive function definition\na closing parenthesis\n"
    | 180 ->
        "079\na recursive functions declaration\nan opening parenthesis to start a list of function declaration\n"
    | 181 ->
        "078\na recursive functions definition\na function declaration of the form \"(name (sort*) sort)\"\n"
    | 182 ->
        "148\na function declaration\na symbol for the function name\n"
    | 183 ->
        "147\na function declaration\nan opening parenthesis to start the list of arguments sorts\n"
    | 184 ->
        "146\na function declaration\neither a sort for the first argument type, or a closing parenthesis\n"
    | 186 ->
        "145\na function declaration\na sort for the return type of the function\n"
    | 187 ->
        "144\na function declaration\na closing parenthesis\n"
    | 195 ->
        "143\na list of function declarations\nanother function declaration, or a closing parenthesis\n"
    | 190 ->
        "077\na recursive functions definition\nan opening parenthesis to start a list the function's bodies\n"
    | 191 ->
        "076\na recursive functions definition\na term for the first function's body\n"
    | 193 ->
        "075\na recursive functions definition\na closing parenthesis\n"
    | 197 ->
        "074\na function definition\na symbol for the function's name\n"
    | 198 ->
        "073\na function definition\na closing parenthesis\n"
    | 200 ->
        "072\na sort declaration\na symbol for the sort name\n"
    | 201 ->
        "071\na sort declaration\na numeral for the arity of the sort being declared\n"
    | 202 ->
        "070\na sort declaration\na closing parenthesis\n"
    | 204 ->
        "069\na function declaration\na symbol for the function's name\n"
    | 205 ->
        "068\na function declaration\nan opening parenthesis to start the list of sorts for the function's arguments\n"
    | 206 ->
        "067\na function declaration\na closing parenthesis, or a list of sorts for the arguments of the function\n"
    | 207 ->
        "142\na list of sorts\nanother sort or a closing parenthesis\n"
    | 210 ->
        "066\na function declaration\na sort for the return type of the function\n"
    | 211 ->
        "065\na function declaration\na closing parenthesis\n"
    | 213 ->
        "064\na datatypes declaration\na list of sort declaration, starting with an opening parenthesis\n"
    | 214 ->
        "063\na datatypes declaration\na parametric sort declaration of the form \"(symbol num)\"\n"
    | 215 ->
        "141\na datatype arity declaration\na symbol for the datatype name\n"
    | 216 ->
        "140\na datatype arity declaration\na numeral for the datatype arity\n"
    | 217 ->
        "139\na datatype arity declaration\na closing parenthesis\n"
    | 219 ->
        "138\na list of datatype arity declarations\nanother datatype arity declaration, or a closing parenthesis\n"
    | 222 ->
        "062\na datatypes declaration\nan opening parenthesis to start a list of datatype definitions,\none for each of the sorts being declared\n"
    | 223 ->
        "061\na datatypes definition\nan opening parenthesis to start a list of constructors for the first defined datatype\n"
    | 253 ->
        "137\na list of datatype declarations\nanother datatype declaration, or a closing parenthesis\n"
    | 251 ->
        "060\na datatypes declaration\na closing parenthesis\n"
    | 255 ->
        "059\na datatype declaration\na symbol\n"
    | 256 ->
        "058\na datatype declaration\nan opening parenthesis to start the datatype declaration\n"
    | 224 ->
        "136\na datatype declaration\na list of constructor declarations of the form \"(symbol selector*)\",\nor a parameterization of the datatype of the form \"par (sort+)\"\n"
    | 225 ->
        "135\na datatype declaration\nan opening parenthesis to start a list of sort parameters for the datatype\n"
    | 226 ->
        "134\na list of sort variables to parameterize a datatype\na symbol\n"
    | 246 ->
        "133\na list of sort variables to parameterize a datatype\nanother symbol, or a closing parenthesis\n"
    | 229 ->
        "132\na datatype declaration\nan opening parenthesis to start the list of constructors\n"
    | 230 ->
        "131\na datatype declaration\na constructor declaration of the form \"(symbol selector*)\"\n"
    | 242 ->
        "130\na datatype declaration\na closing parenthesis\n"
    | 231 ->
        "129\na constructor declaration\na symbol for the constructor name\n"
    | 232 ->
        "128\na constructor declaration\na selector declaration, of the form \"(selector sort)\", or a closing parenthesis\n"
    | 233 ->
        "127\na selector declaration\na symbol for the selector name\n"
    | 234 ->
        "126\na selector declaration\na sort for the return type of the selector\n"
    | 235 ->
        "125\na selector declaration\na closing parenthesis\n"
    | 237 ->
        "124\na list of selectors\nanother selector of the form \"(selector sort)\", or a closing parenthesis\n"
    | 244 ->
        "123\na list of constructor declarations\nanother constructor declaration of the form \"(constructor selectors*)\",\nor a closing parenthesis\n"
    | 257 ->
        "057\na datatype declaration\na closing parenthesis\n"
    | 259 ->
        "056\na constant declaration\na symbol;\nnote that keywords and reserved words (such as '_', 'as', ...) are not\nsymbols, and thus are not allowed here\n"
    | 260 ->
        "055\na constant declaration\na sort\n"
    | 261 ->
        "054\na constant declaration\na closing parenthesis\n"
    | 61 ->
        "122\na sort\na sort to start a non-empty list of arguments\n"
    | 62 ->
        "121\na list of sorts\na sort, or a closing parenthesis\n"
    | 60 ->
        "120\na sort\nan identifier to make a sort function application (such as \"f x y\"),\nor an underscore to start an indexed identifier\n"
    | 263 ->
        "053\na check-sat-assuming command\na list of propositional literals, starting with an opening parenthesis\n"
    | 264 ->
        "052\na list of propositional literals\na propositional literal, i.e. either a symbol or the negation of a symbol\n"
    | 272 ->
        "119\na list of propositional literals\na propositional literal of the form \"symbol\" or \"(not symbol)\"\n"
    | 265 ->
        "117\na propositional literal\nthe \"not\" symbol\n"
    | 267 ->
        "047\na propositional literal\na symbol\n"
    | 268 ->
        "046\na propositional literal\na closing parenthesis\n"
    | 275 ->
        "051\na check-sat-assuming command\na closing parenthesis\n"
    | 277 ->
        "050\na check-sat command\na closing parenthesis\n"
    | 279 ->
        "048\na term\na term construction (symbol, function application, match, let binding, ...);\nnote that keywords and reserved words (such as '_', 'as', ...) are\nnot symbols, and thus are not allowed here\n"
    | 280 ->
        "049\nan assertion\na closing parenthesis\n"
    | 128 ->
        "044\na function application\na term as argument;\nnote that keywords and reserved words (such as '_', 'as', ...) are\nnot terms, and thus are not allowed here\n"
    | 46 ->
        "042\na term\na term construction (identifier, let binding, quantification, ...);\nnote that this expectation if caused by the preceding opening parenthesis\n"
    | 69 ->
        "038\na match\na term to match (i.e. the scrutinee of the match)\n"
    | 70 ->
        "037\na match\na match case list, starting with an opening parenthesis\n"
    | 71 ->
        "036\na list of match cases\na match case of the form \"(pattern term)\"\n"
    | 88 ->
        "031\na match\na closing parenthesis to close the match\n"
    | 92 ->
        "027\na term\na variable binding list, starting with an opening parenthesis\n"
    | 93 ->
        "026\na term\na variable binding of the form \"(var term)\"\n"
    | 101 ->
        "021\na term\na term (body for the let binding)\n"
    | 102 ->
        "020\na term\na closing parenthesis to end the let binding\n"
    | 104 ->
        "019\na term\na list of sorted variables, starting with an opening parenthesis\n"
    | 105 ->
        "018\na term\na sorted variable of the form \"(var sort)\"\n"
    | 113 ->
        "013\na term\na term (body for the universal quantification)\n"
    | 114 ->
        "012\na term\na closing parenthesis to end the universally quantified formula\n"
    | 116 ->
        "011\na term\na list of sorted variables, starting with an opening parenthesis\n"
    | 117 ->
        "010\na term\na sorted variable of the form \"(var sort)\"\n"
    | 119 ->
        "009\na term\na term (body for the existencial quantification)\n"
    | 120 ->
        "008\na term\na closing parenthesis to end the existencially quantified formula\n"
    | 122 ->
        "007\na term with attribute\na term.\n"
    | 123 ->
        "006\nattributes for a term\nan attribute of the form \"keyword value\"\n"
    | 287 ->
        "116\nan input statement\nan opening parenthesis to start a command\n"
    | 288 ->
        "115\na command\na command name\n"
    | 289 ->
        "114\na set-option command\nan attribute of the form \"keyword value?\"\n"
    | 290 ->
        "113\na set-option command\na closing parenthesis, or an attribute value;\nnote that keywords and reserved words (such as '_', 'as', ...) are not\nvalid attribute values, and thus are not allowed here\n"
    | 292 ->
        "112\na set-logic command\na symbol for the logic name\n"
    | 293 ->
        "111\na set-logic command\na closing parenthesis\n"
    | 295 ->
        "110\na set-info command\nan attribute of the form \"keyword value?\"\n"
    | 296 ->
        "109\na set-info command\na closing parenthesis, or an attribute value;\nnote that keywords and reserved words (such as '_', 'as', ...) are not\nvalid attribute values, and thus are not allowed here\n"
    | 298 ->
        "108\na reset-assertions command\na closing parenthesis\n"
    | 300 ->
        "107\na reset command\na closing parenthesis\n"
    | 302 ->
        "106\na push command\na numeral\n"
    | 303 ->
        "105\na push command\na closing parenthesis\n"
    | 305 ->
        "104\na pop command\na numeral\n"
    | 306 ->
        "103\na pop command\na closing parenthesis\n"
    | 308 ->
        "102\na get-value command\nan opening parenthesis to start a list of terms\n"
    | 309 ->
        "101\na get-value command\na term\n"
    | 311 ->
        "100\na get-value command\na closing parenthesis\n"
    | 313 ->
        "099\na get-unsat-core command\na closing parenthesis\n"
    | 315 ->
        "098\na get-unsat-assumptions command\na closing parenthesis\n"
    | 317 ->
        "097\na get-proof command\na closing parenthesis\n"
    | 319 ->
        "096\na get-option command\na keyword of the form \":symbol\"\n"
    | 320 ->
        "095\na get-option command\na closing parenthesis\n"
    | 322 ->
        "094\na get-model command\na closing parenthesis\n"
    | 324 ->
        "093\na get-info command\na keyword of the form \":symbol\"\n"
    | 325 ->
        "092\na get-info command\na closing parenthesis\n"
    | 327 ->
        "091\na get-assignment command\na closing parenthesis\n"
    | 329 ->
        "090\na get-assertions command\na closing parenthesis\n"
    | 331 ->
        "089\nan exit command\na closing parenthesis\n"
    | 333 ->
        "088\nan echo command\na string literal\n"
    | 334 ->
        "087\nan echo command\na closing parenthesis\n"
    | 336 ->
        "086\na sort definition\na symbol for the defined sort's name\n"
    | 337 ->
        "085\na sort definition\nan opening parenthesis to start a list of arguments\n"
    | 338 ->
        "084\na sort definition\na closing parenthesis, or a list of symbols for the definition arguments\n"
    | 340 ->
        "083\na sort definition\na sort for the definition body\n"
    | 341 ->
        "082\na sort definition\na closing parenthesis\n"
    | 343 ->
        "081\na recursive function definition\na symbol for the function's name\n"
    | 344 ->
        "080\na recursive function definition\na closing parenthesis\n"
    | 346 ->
        "079\na recursive functions declaration\nan opening parenthesis to start a list of function declaration\n"
    | 347 ->
        "078\na recursive functions definition\na function declaration of the form \"(name (sort*) sort)\"\n"
    | 349 ->
        "077\na recursive functions definition\nan opening parenthesis to start a list the function's bodies\n"
    | 350 ->
        "076\na recursive functions definition\na term for the first function's body\n"
    | 352 ->
        "075\na recursive functions definition\na closing parenthesis\n"
    | 354 ->
        "074\na function definition\na symbol for the function's name\n"
    | 355 ->
        "073\na function definition\na closing parenthesis\n"
    | 357 ->
        "072\na sort declaration\na symbol for the sort name\n"
    | 358 ->
        "071\na sort declaration\na numeral for the arity of the sort being declared\n"
    | 359 ->
        "070\na sort declaration\na closing parenthesis\n"
    | 361 ->
        "069\na function declaration\na symbol for the function's name\n"
    | 362 ->
        "068\na function declaration\nan opening parenthesis to start the list of sorts for the function's arguments\n"
    | 363 ->
        "067\na function declaration\na closing parenthesis, or a list of sorts for the arguments of the function\n"
    | 365 ->
        "066\na function declaration\na sort for the return type of the function\n"
    | 366 ->
        "065\na function declaration\na closing parenthesis\n"
    | 368 ->
        "064\na datatypes declaration\na list of sort declaration, starting with an opening parenthesis\n"
    | 369 ->
        "063\na datatypes declaration\na parametric sort declaration of the form \"(symbol num)\"\n"
    | 371 ->
        "062\na datatypes declaration\nan opening parenthesis to start a list of datatype definitions,\none for each of the sorts being declared\n"
    | 372 ->
        "061\na datatypes definition\nan opening parenthesis to start a list of constructors for the first defined datatype\n"
    | 374 ->
        "060\na datatypes declaration\na closing parenthesis\n"
    | 376 ->
        "059\na datatype declaration\na symbol\n"
    | 377 ->
        "058\na datatype declaration\nan opening parenthesis to start the datatype declaration\n"
    | 378 ->
        "057\na datatype declaration\na closing parenthesis\n"
    | 380 ->
        "056\na constant declaration\na symbol;\nnote that keywords and reserved words (such as '_', 'as', ...) are not\nsymbols, and thus are not allowed here\n"
    | 381 ->
        "055\na constant declaration\na sort\n"
    | 382 ->
        "054\na constant declaration\na closing parenthesis\n"
    | 384 ->
        "053\na check-sat-assuming command\na list of propositional literals, starting with an opening parenthesis\n"
    | 385 ->
        "052\na list of propositional literals\na propositional literal, i.e. either a symbol or the negation of a symbol\n"
    | 387 ->
        "051\na check-sat-assuming command\na closing parenthesis\n"
    | 389 ->
        "050\na check-sat command\na closing parenthesis\n"
    | 391 ->
        "048\na term\na term construction (symbol, function application, match, let binding, ...);\nnote that keywords and reserved words (such as '_', 'as', ...) are\nnot symbols, and thus are not allowed here\n"
    | 392 ->
        "049\nan assertion\na closing parenthesis\n"
    | 397 ->
        "046\na term\na term construction (symbol, function application, match, let binding, ...);\nnote that keywords and reserved words (such as '_', 'as', ...) are\nnot symbols, and thus are not allowed here\n"
    | 401 ->
        "041\nan indexed identifier\na symbol;\nnote that keywords and reserved words (such as '_', 'as', ...) are not\nsymbols, and thus are not allowed here\n"
    | 402 ->
        "040\nan indexed identifier\nan index, i.e. either a numeral, a symbol, or a hexadecimal number;\nnote that keywords and reserved words (such as '_', 'as', ...) are not\nsymbols, and thus are not allowed here\n"
    | 54 ->
        "045\nan index list\neither a closing parenthesis, or an index (i.e. a numeral, a symbol,\nor a hexadecimal);\nnote that keywords and reserved words (such as '_', 'as', ...) are\nnot symbols, and thus are not allowed here\n"
    | 437 ->
        "044\na function application\na term as argument;\nnote that keywords and reserved words (such as '_', 'as', ...) are\nnot terms, and thus are not allowed here\n"
    | 129 ->
        "043\na list of terms\neither a closing parenthesis, or another term;\nnote that keywords and reserved words (such as '_', 'as', ...) are\nnot terms, and thus are not allowed here\n"
    | 400 ->
        "042\na term\na term construction (identifier, let binding, quantification, ...);\nnote that this expectation if caused by the preceding opening parenthesis\n"
    | 47 ->
        "041\nan indexed identifier\na symbol;\nnote that keywords and reserved words (such as '_', 'as', ...) are not\nsymbols, and thus are not allowed here\n"
    | 48 ->
        "040\nan indexed identifier\nan index, i.e. either a numeral, a symbol, or a hexadecimal number;\nnote that keywords and reserved words (such as '_', 'as', ...) are not\nsymbols, and thus are not allowed here\n"
    | 56 ->
        "039\nan identifier in parentheses\neither an indexed identifier (starting with an underscore)\nor an 'as' type ascription;\nnote that this is because of the preceding opening parenthesis\n"
    | 57 ->
        "004\na qualified identifier\nan identifier.\nNote that keywords (such as '_', 'as', ...) are not identifiers,\nand thus are not allowed here.\n"
    | 59 ->
        "003\na qualified identifier\na sort, i.e. either an identifier, or a sort constructor application;\nnote that keywords (such as '_', 'as', ...) are none of these, and thus\nare not allowed here.\n"
    | 67 ->
        "002\na qualified identifier\na closing parenthesis\n"
    | 405 ->
        "038\na match\na term to match (i.e. the scrutinee of the match)\n"
    | 406 ->
        "037\na match\na match case list, starting with an opening parenthesis\n"
    | 407 ->
        "036\na list of match cases\na match case of the form \"(pattern term)\"\n"
    | 72 ->
        "035\na match case\na pattern, i.e. either a symbol or a datatype pattern of\nthe form \"(symbol symbol+)\";\nnote that keywords and reserved words (such as '_', 'as', ...) are not\nsymbols, and thus are not allowed here\n"
    | 81 ->
        "034\na match case\na term for the case body\n"
    | 82 ->
        "033\na match case\na closing parenthesis to close the match case\n"
    | 90 ->
        "032\na list of match cases\na closing parenthesis or a match case of the form \"(pattern body)\"\n"
    | 409 ->
        "031\na match\na closing parenthesis to close the match\n"
    | 74 ->
        "030\na pattern\na symbol (either a variable or a datatype constructor);\nnote that keywords and reserved words (such as '_', 'as', ...) are not\nsymbols, and thus are not allowed here\n"
    | 75 ->
        "029\narguments of a constructor in a pattern\na symbol to bind the first constructor argument;\nnote that keywords and reserved words (such as '_', 'as', ...) are not\nsymbols, and thus are not allowed here\n"
    | 76 ->
        "028\narguments of a constructor in a pattern\na closing parenthesis, or a symbol to bind the argument;\nnote that keywords and reserved words (such as '_', 'as', ...) are not\nsymbols, and thus are not allowed here\n"
    | 411 ->
        "027\na term\na variable binding list, starting with an opening parenthesis\n"
    | 412 ->
        "026\na term\na variable binding of the form \"(var term)\"\n"
    | 94 ->
        "025\na variable binding\na symbol (i.e. variable name)\n"
    | 95 ->
        "024\na variable binding\na term\n"
    | 96 ->
        "023\na variable binding\na closing parenthesis\n"
    | 98 ->
        "022\na list of variable binding\na closing parenthesis or a variable binding of the form \"(var term)\"\n"
    | 414 ->
        "021\na term\na term (body for the let binding)\n"
    | 415 ->
        "020\na term\na closing parenthesis to end the let binding\n"
    | 417 ->
        "019\na term\na list of sorted variables, starting with an opening parenthesis\n"
    | 418 ->
        "018\na term\na sorted variable of the form \"(var sort)\"\n"
    | 106 ->
        "017\na sorted variable\na symbol, i.e. a variable name\n"
    | 107 ->
        "016\na sorted variable\na sort, i.e. either an identifier, or a sort constructor application;\nnote that keywords and reserved words (such as '_', 'as', ...) are not\nidentifiers, and thus are not allowed here\n"
    | 108 ->
        "015\na sorted variable\na closing parenthesis\n"
    | 110 ->
        "014\na list of sorted variables\neither a closing parentheis, or a sorted var of the form \"(var sort)\"\n"
    | 420 ->
        "013\na term\na term (body for the universal quantification)\n"
    | 421 ->
        "012\na term\na closing parenthesis to end the universally quantified formula\n"
    | 423 ->
        "011\na term\na list of sorted variables, starting with an opening parenthesis\n"
    | 424 ->
        "010\na term\na sorted variable of the form \"(var sort)\"\n"
    | 426 ->
        "009\na term\na term (body for the existencial quantification)\n"
    | 427 ->
        "008\na term\na closing parenthesis to end the existencially quantified formula\n"
    | 429 ->
        "007\na term with attribute\na term\n"
    | 430 ->
        "006\na term\nan attribute of the form \"keyword value\"\n"
    | 126 ->
        "005\nan attribute list\neither a closing parenthesis, or another attribute of the form\n\"keyword value\"\n"
    | 433 ->
        "004\na qualified identifier\nan identifier;\nnote that keywords and reserved words (such as '_', 'as', ...) are not\nidentifiers, and thus are not allowed here\n"
    | 434 ->
        "003\na qualified identifier\na sort, i.e. either an identifier, or a sort constructor application;\nnote that keywords and reserved words (such as '_', 'as', ...) are not\nidentifiers, and thus are not allowed here\n"
    | 435 ->
        "002\na qualified identifier\na closing parenthesis\n"
    | 58 ->
        "001\nan identifier\nan underscore: identifiers starting with an opening parenthesis must be\nindexed identifiers, of the form \"(_ symbol index+)\"\n"
    | _ ->
        raise Not_found