Currently we allow sat calls on Goal. That's just fine. But we also allow prove calls on Goal's. That's semantically fine too, but is a bit bizarre. Would be nice to be able to do the former but not the latter.
Unfortunately, my experiment with this in the provableAndSatisfiable branch didn't go too far; it lead to a lot of code, and also didn't accomplish the task:
- REJECT: prove $ \x -> (do { constrain ( x .> (5::SInteger)) } :: Goal)
- REJECT: prove (pure () :: Goal)
- ACCEPT: sat $ \x -> (do { constrain ( x .> (5::SInteger)) } :: Goal)
- ACCEPT: sat (pure () :: Goal)
Currently we allow sat calls on Goal. That's just fine. But we also allow prove calls on Goal's. That's semantically fine too, but is a bit bizarre. Would be nice to be able to do the former but not the latter.
Unfortunately, my experiment with this in the
provableAndSatisfiablebranch didn't go too far; it lead to a lot of code, and also didn't accomplish the task:Perhaps this idea can be revisited at some point.