vstd_extra/trans_macros.rs
1use vstd::prelude::*;
2
3use crate::panic::*;
4
5#[macro_export]
6macro_rules! assert {
7 ($cond:expr) => {
8 if !($cond) {
9 $crate::panic::panic_diverge()
10 }
11 };
12 ($cond:expr, $msg:literal) => {
13 if !($cond) {
14 $crate::panic::panic_diverge()
15 }
16 };
17}
18
19#[macro_export]
20macro_rules! assert_eq {
21 ($l:expr, $r:expr) => {
22 if ($l != $r) {
23 $crate::panic::panic_diverge()
24 }
25 };
26}