TreeNodeValue

vstd_extra::ghost_tree

Trait TreeNodeValue 

Source 
pub trait TreeNodeValue<const L: usize>: Sized + Inv {
    // Required methods
    spec fn default(lv: nat) -> Self;
    proof fn default_preserves_inv();
    spec fn la_inv(self, lv: nat) -> bool;
    proof fn default_preserves_la_inv();
    spec fn rel_children(self, index: int, child: Option<Self>) -> bool;
    proof fn default_preserves_rel_children(self, lv: nat);
}

Required Methods§

Source

spec fn default(lv: nat) -> Self

Source

proof fn default_preserves_inv()

ensures
forall |lv: nat| #[trigger] Self::default(lv).inv(),
Source

spec fn la_inv(self, lv: nat) -> bool

Source

proof fn default_preserves_la_inv()

ensures
forall |lv: nat| #[trigger] Self::default(lv).la_inv(lv),
Source

spec fn rel_children(self, index: int, child: Option<Self>) -> bool

Source

proof fn default_preserves_rel_children(self, lv: nat)

requires
self.inv(),
self.la_inv(lv),
ensures
forall |i: int| #[trigger] self.rel_children(i, Some(Self::default(lv + 1))),

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors§