search

Whiley / WhileyTheoremProver

The Whiley Theorem Prover (WyTP) is an automatic and interactive theorem prover designed to discharge verification conditions generated by the Whiley Compiler. WyTP operates over a variant of first-order logic which includes integer arithmetic, arrays and quantification.
Apache License 2.0
8 stars 2 forks source link

Problem Parsing Qualified Expressions #97

Closed DavePearce closed 7 years ago

DavePearce commented 7 years ago

The following seems to be failing to parse:

function f(int x)->(int r)

assert:
    forall(int x):
        test.f(x) == test.f(x)

This generates the following error:

./test.wyal:5: unrecognised term
        test.f(x) == test.f(x)
        ^^^^