Zulip Chat Archive

Stream: new members

Topic: asserting a structure produces an error


view this post on Zulip Julian Berman (Oct 11 2020 at 14:54):

Is there a testing helper or something that I can use to assert that the second example below produces an error?

import tactic

structure foo :=
(value : )
(istwelve : value = 12 . tactic.exact_dec_trivial)

example : foo := { foo . value := 12 }

-- assertBlowsUp
example : foo := { foo . value := 13 }

view this post on Zulip Anne Baanen (Oct 12 2020 at 09:58):

Maybe docs#tactic.success_if_fail helps?

view this post on Zulip Julian Berman (Oct 12 2020 at 13:52):

Thanks! Appreciate the pointer, will see if I can use that.


Last updated: May 15 2021 at 02:11 UTC