Macro declare_namespace
declare_namespace!() { /* proc-macro */ }Expand description
Declare a new namespace.
ยงExample
use creusot_contracts::{ghost::local_invariant::{declare_namespace, Namespace}, logic::Set, prelude::*};
declare_namespace! { A }
#[requires(ns.contains(A()))]
fn foo(ns: Ghost<&mut Set<Namespace>>) { /* ... */ }