hydro_lang/
unsafety.rs

1#[derive(Copy, Clone)]
2pub struct NonDet;
3
4#[macro_export]
5/// Fulfills a non-determinism guard parameter by declaring a reason why the
6/// non-determinism is tolerated or providing other non-determinism guards
7/// that forward the inner non-determinism.
8///
9/// The first argument must be a string literal with the reason the non-determinism
10/// is okay. If forwarding a parent non-determinism, you should provide a short
11/// explanation of how the inner non-determinism is captured by the outer one,
12/// and also discuss any forms of the inner non-determinism that will not be exposed
13/// outside if they are locally resolved
14macro_rules! nondet {
15    ($(#[doc = $doc:expr])+$($forward:ident),*) => {
16        {
17            $(let _ = $forward;)*
18            $crate::unsafety::NonDet
19        }
20    };
21}