No analog of assert forall by
for forall_arith
; deprecate forall_arith
?
#601
Closed
jaylorch
started this conversation in
Language design
Replies: 3 comments
-
Maybe the thing to do is to combine |
Beta Was this translation helpful? Give feedback.
0 replies
-
Addressed by #625. Shall we deprecate |
Beta Was this translation helpful? Give feedback.
0 replies
-
|
Beta Was this translation helpful? Give feedback.
0 replies
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
-
It would be nice if one could do
assert forall_arith |x| <some arithmetic expression> by { <proof> }
to establishforall_arith |x| <some arithmetic expression>
, analogously to how one can doassert forall |x| <some normal expression> by { <proof> }
.Beta Was this translation helpful? Give feedback.
All reactions