digama0
commented
4 years ago This is controlled by the delimiter command. delimiter $ left delims $ $ right delims $; declares a bunch of left and right delimiter characters (a character can be both, and in the form delimiter $ both delims $; all characters in the list are declared as both). A token is a maximal sequence of non-whitespace tokens, except that tokens are always broken after a left delimiter and before a right delimiter. So for example if ( is a left and ) is a right delimiter, then )x( is one token but (x) is three.
In set.mm0, ~ is declared as a both delimiter (this file was written before there were separate left and right delimiters; today I would declare this as a left delimiter), meaning that it always exists as a token on its own even if there are no whitespaces around it. x~~ph gets tokenized as x ~ ~ ph.
Lakedaemon
In the current set.mm0, shouldn't def wa (ph ps: wff): wff = $ ~(ph -> ~ps) $; be instead def wa (ph ps: wff): wff = $ ~(ph -> ~ ps) $; because the dynamic parser would not recognize "tilde+ps" as the 2 tokens "tilde" and "ph" ? Or am I wrong ?