declare_namespace

Macro declare_namespace 

declare_namespace!() { /* proc-macro */ }
Expand description

Declare a new namespace.

ยงExample

use creusot_std::{ghost::invariant::{declare_namespace, Namespace}, logic::Set, prelude::*};
declare_namespace! { A }

#[requires(ns.contains(A()))]
fn foo(ns: Ghost<&mut Set<Namespace>>) { /* ... */ }