declare_namespace

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>>) { /* ... */ }