Skip to main content

HasObligations

vstd_extra::drop_tracking

Trait HasObligations 

Source 
pub trait HasObligations<K> {
    // Required method
    spec fn obligations(self) -> Set<K>;
}
Expand description

State that carries an obligation ledger keyed by K.

Required Methods§

Source

spec fn obligations(self) -> Set<K>

Implementors§