diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-01-07 17:06:33 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-07 14:06:33 -0600 |
| commit | 94c687bb12f3ba89225886b3b3eeea3f0dfdfd0a (patch) | |
| tree | 439975ec225bff05c578fb0b97a7c6da505523a1 /src/parser/tptp/Tptp.g | |
| parent | 3b0b4f554841847aa529a1d95585aedcba5b0fee (diff) | |
Fix warning in TPTP parser (#5752)
Diffstat (limited to 'src/parser/tptp/Tptp.g')
| -rw-r--r-- | src/parser/tptp/Tptp.g | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 6b66b5422..0c16e472d 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -921,7 +921,7 @@ thfQuantifier[CVC4::api::Kind& kind] | LAMBDA_TOK { kind = api::LAMBDA; } | CHOICE_TOK { - UNSUPPORTED("Choice operator"); + UNSUPPORTED("Choice operator"); } | DEF_DESC_TOK { @@ -1621,7 +1621,7 @@ NOT_TOK : '~'; FORALL_TOK : '!'; EXISTS_TOK : '?'; LAMBDA_TOK : '^'; -WITNESS_TOK : '@+'; +CHOICE_TOK : '@+'; DEF_DESC_TOK : '@-'; AND_TOK : '&'; IFF_TOK : '<=>'; |