Modal example in USAGE.md doesn't work in latest release

[Tc14Hd]

The modal example found in USAGE.md throws a syntax error in the latest release.

Example

thf(simple_b, logic, ( $modal == [
    $constants == $rigid ,
    $quantification == $constant ,
    $consequence == $global ,
    $modalities == $modal_system_S5 ] ) ).

thf(axiom_B, conjecture, ( ![A:$o]: ( A => ( [.] @ ( <.> @ A ) ) ) )).

Output

% [INFO]     Parsing problem modal-problem ... 
% OUT OF CHEESE ERROR +++ MELON MELON MELON +++ REDO FROM START
% SZS status SyntaxError for modal-problem : Parse error in file 'modal-problem' in line 1:32. Unrecognized thf formula input 'EQUALS'

I used the command java -jar leo3-v1.6.jar modal-problem to run the example.

[lex-lex]

Thanks for the report; I forgot to update those examples. The description is updated and also extended now.

Best, Alex

[Tc14Hd]

Thanks for the fast response, but I'm still getting the same error. Maybe I have to build on my own instead of using the pre-built binary.

[lex-lex]

Ah, I see. Yes, there was a rather disruptive change in the syntax as we were further working and enhancing it (see also here: https://arxiv.org/abs/2202.09836). You'll need Leo-III >= 1.6.7 to work with the new examples; there is no official release yet but you can retrieve the sources from tags (e.g., https://github.com/leoprover/Leo-III/releases/tag/v1.6.9) and build it from these sources, sorry for that.

Alternatively, for your convenience, I uploaded an executable jar of v1.6.9 to https://alexandersteen.de/files/leo3/leo3-v1.6.9.jar

[Tc14Hd]

Thank you!