Open
Description
Currently all term evaluation gets stuck, so we end up with terms like 1 + 1. It's not possible to prove things like P(1 + 1) |- P(2) without the Z3 rule, but it should be.
{{ message }}
No one assigned
No type
No projects
No milestone
None yet
No branches or pull requests