|
|
LAMBDA = '\\' |
|
|
LAMBDA_LIST = ['\\'] |
|
|
EXISTS = 'exists' |
|
|
EXISTS_LIST = ['some', 'exists', 'exist'] |
|
|
ALL = 'all' |
|
|
ALL_LIST = ['all', 'forall'] |
|
|
DOT = '.' |
|
|
OPEN = '(' |
|
|
CLOSE = ')' |
|
|
COMMA = ',' |
|
|
NOT = '-' |
|
|
NOT_LIST = ['not', '-', '!'] |
|
|
AND = '&' |
|
|
AND_LIST = ['and', '&', '^'] |
|
|
OR = '|' |
|
|
OR_LIST = ['or', '|'] |
|
|
IMP = '->' |
|
|
IMP_LIST = ['implies', '->', '=>'] |
|
|
IFF = '<->' |
|
|
IFF_LIST = ['iff', '<->', '<=>'] |
|
|
EQ = '=' |
|
|
EQ_LIST = ['=', '=='] |
|
|
NEQ = '!=' |
|
|
NEQ_LIST = ['!='] |
|
|
BINOPS = ['and', '&', '^', 'or', '|', 'implies', '->', '=>', '... |
|
|
QUANTS = ['some', 'exists', 'exist', 'all', 'forall'] |
|
|
PUNCT = ['.', '(', ')', ','] |
|
|
TOKENS = ['and', '&', '^', 'or', '|', 'implies', '->', '=>', '... |
|
|
SYMBOLS = ['&', '^', '|', '->', '=>', '<->', '<=>', '=', '==',... |
|
|
NLTK = 1
|
|
|
OLD_NLTK = 0
|
|
|
PROVER9 = 2
|
|
|
x = '!' |