New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Logical IFF #137

Closed
DavePearce opened this Issue Oct 8, 2017 · 1 comment

Comments

Projects
None yet
1 participant
@DavePearce
Member

DavePearce commented Oct 8, 2017

Currently, the logical iff operator <==> is not supported. This previously wasn't a problem as WyC translated this into disjunctions for us. But, the latest version of WyC supports <==> all the way through. A simple example:

assert:
    forall(int x):
        (x > 0) <==> (x > 0)

DavePearce added a commit that referenced this issue Oct 8, 2017

Add Support for Logical IFF #137
This adds support for breaking down the logical iff operator into a
union of two conjuncts.  Here, a <==> b becomes (a&&b)||(!a&&!b).

Most of the machinery for dealing with the iff operator was already in
place.  For example, it was already being parsed etc.
@DavePearce

This comment has been minimized.

Member

DavePearce commented Oct 8, 2017

Fixed.

@DavePearce DavePearce closed this Oct 8, 2017

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment