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}
27
28#[macro_export]
29macro_rules! debug_assert {
30    ($cond:expr) => {
31        #[cfg(debug_assertions)]
32        if !($cond) {
33            $crate::panic::panic_diverge()
34        }
35    };
36    ($cond:expr, $msg:literal) => {
37        #[cfg(debug_assertions)]
38        if !($cond) {
39            $crate::panic::panic_diverge()
40        }
41    };
42}
vstd_extra/trans_macros.rs

vstd_extra/
trans_macros.rs
