Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Unify post-condition verification types and functions.
We don't need to pattern match on different types of failures: we only need to be able to pretty-print any failures that occur. Therefore, we can remove the outer algebraic types, which are just boilerplate, and generalize the way in which we represent verification failures.
- Loading branch information