Skip to main content

TreeNode

vstd_extra::ghost_tree

Struct TreeNode 

Source 
pub struct TreeNode<T: TreeNodeValue<L>, const N: usize, const L: usize> { /* private fields */ }
Expand description

A ghost tree node with depth L and N children.

Each tree node has a value of type T and a sequence of children, forming a subtree. The length of the child seuquence is fixed at N, while the absence of a child is represeneted with Option::None. The maximum depth of the tree is L.

Implementations§

Source§

impl<T: TreeNodeValue<L>, const N: usize, const L: usize> TreeNode<T, N, L>

Source

pub closed spec fn value(self) -> T

Returns the value stored in this node.

Source

pub closed spec fn level(self) -> nat

Returns the level of this node.

Source

pub closed spec fn children(self) -> Seq<Option<Self>>

Returns the sequence of children.

Source

pub open spec fn has_child(self, i: int) -> bool

{ self.children()[i] is Some }

Returns whether the i-th child exists.

Source

pub open spec fn child(self, i: int) -> Self

{ self.children()[i]->0 }

Returns the i-th child. Only valid when it exists.

Source

pub open spec fn size() -> nat

{ N as nat }
Source

pub open spec fn max_depth() -> nat

{ L as nat }
Source

pub closed spec fn new(value: T, level: nat, children: Seq<Option<Self>>) -> Self

Constructs a node from its fields.

Source

pub proof fn tracked_new(tracked value: T, level: nat, tracked children: Seq<Option<Self>>) -> tracked Self

returns
Self::new(value, level, children),

Constructs a tracked node from its tracked fields.

Source

pub open spec fn new_default(lv: nat) -> Self

{ Self::new(T::default(lv), lv, Seq::new(N as nat, |i| None)) }

Constructs a node at the given level with default value and no children.

Source

pub open spec fn new_val(val: T, lv: nat) -> Self

recommends
lv < L,
{ Self::new(val, lv, Seq::new(N as nat, |i| None)) }

Constructs a node with a given value and level, without childrens.

Source

pub open spec fn inv_node(self) -> bool

{
    &&& self.value().inv()
    &&& self.value().la_inv(self.level())
    &&& self.level() < L
    &&& self.children().len() == Self::size()

}
Source

pub open spec fn inv_children(self) -> bool

{
    if self.level() == L - 1 {
        forall |i: int| 0 <= i < Self::size() ==> #[trigger] self.children()[i] is None
    } else {
        forall |i: int| {
            0 <= i < Self::size()
                ==> match #[trigger] self.children()[i] {
                    Some(child) => (
                        &&& child.level() == self.level() + 1
                        &&& self.value().rel_children(i, Some(child.value()))

                    ),
                    None => self.value().rel_children(i, None),
                }
        }
    }
}
Source

pub open spec fn inv(self) -> bool

{
    &&& L > 0
    &&& N > 0
    &&& self.inv_node()
    &&& self.inv_children()
    &&& if L - self.level() == 1 {
        true
    } else {
        forall |i: int| {
            0 <= i < Self::size()
                ==> match #[trigger] self.children()[i] {
                    Some(child) => child.inv(),
                    None => true,
                }
        }
    }

}
Source

pub broadcast proof fn lemma_new_properties(value: T, level: nat, children: Seq<Option<Self>>)

ensures
Self::new(value, level, children).value() == value,
Self::new(value, level, children).level() == level,
Self::new(value, level, children).children() == children,
Source

pub broadcast proof fn lemma_new_val_properties(val: T, lv: nat)

ensures
Self::new_val(val, lv).value() == val,
Self::new_val(val, lv).level() == lv,
Self::new_val(val, lv).children() == Seq::new(N as nat, |i| None),
Source

pub broadcast proof fn lemma_ext_equal(self, other: Self)

requires
self.value() == other.value(),
self.level() == other.level(),
self.children() =~= other.children(),
ensures
self == other,

Two nodes are equal when all of their observable fields are equal.

Source

pub proof fn tracked_borrow_child(tracked &self, i: int) -> tracked ret : &Self

requires
0 <= i < self.children().len(),
self.children()[i] is Some,
ensures
*ret == self.children()[i]->0,

Borrows a child from the underlying sequence.

Source

pub proof fn tracked_borrow_mut_child(tracked &mut self, i: int) -> tracked ret : &mut Self

requires
0 <= i < self.children().len(),
self.children()[i] is Some,
ensures
*ret == old(self).children()[i]->0,
final(self).value() == old(self).value(),
final(self).level() == old(self).level(),
final(self).children() == old(self).children().update(i, Some(*final(ret))),

Mutably borrows a child from the underlying sequence.

Source

pub proof fn tracked_borrow_value(tracked &self) -> tracked res : &T

ensures
*res == self.value(),
Source

pub proof fn tracked_borrow_mut_value(tracked &mut self) -> tracked res : &mut T

ensures
*res == old(self).value(),
final(self).value() == *final(res),
final(self).level() == old(self).level(),
final(self).children() == old(self).children(),
Source

pub proof fn tracked_into_parts(tracked self) -> tracked (T, Seq<Option<Self>>)

ensures
value == self.value(),
children == self.children(),

Consumes this node and returns its tracked value and children.

Source

pub open spec fn subtree_satisfies( self, path: TreePath<N>, f: FnSpec<(T, TreePath<N>), bool>, ) -> bool

{
    if self.level() < L - 1 {
        &&& f(self.value(), path)
        &&& forall |i: int| {
            0 <= i < self.children().len()
                ==> ((#[trigger] self.has_child(i))
                    ==> self.child(i).subtree_satisfies(path.push_tail(i), f))
        }

    } else {
        &&& f(self.value(), path)

    }
}

Requires f to hold for this node and every present descendant.

path identifies the current node. When descending through child index i, the corresponding child path is path.push_tail(i).

Source

pub proof fn lemma_subtree_satisfies_unroll_once( self, path: TreePath<N>, f: FnSpec<(T, TreePath<N>), bool>, i: int, )

requires
self.inv(),
self.level() < L - 1,
0 <= i < self.children().len(),
self.has_child(i),
self.subtree_satisfies(path, f),
ensures
self.child(i).subtree_satisfies(path.push_tail(i), f),
Source

pub open spec fn implies( f: FnSpec<(T, TreePath<N>), bool>, g: FnSpec<(T, TreePath<N>), bool>, ) -> bool

{
    forall |value: T, path: TreePath<N>| {
        value.inv() ==> (f(value, path) ==> #[trigger] g(value, path))
    }
}
Source

pub proof fn lemma_subtree_satisfies_implies( self, path: TreePath<N>, f: FnSpec<(T, TreePath<N>), bool>, g: FnSpec<(T, TreePath<N>), bool>, )

requires
self.inv(),
Self::implies(f, g),
Self::subtree_satisfies(self, path, f),
ensures
Self::subtree_satisfies(self, path, g),
Source

pub proof fn lemma_new_default_subtree_satisfies( lv: nat, path: TreePath<N>, f: FnSpec<(T, TreePath<N>), bool>, )

requires
lv < L,
Self::new_default(lv).inv(),
f(T::default(lv), path),
ensures
Self::new_default(lv).subtree_satisfies(path, f),

If f(T::default(lv), path), then TreeNode::new_default(lv).subtree_satisifies(path,f).

Source

pub proof fn lemma_new_val_subtree_satisfies( val: T, lv: nat, path: TreePath<N>, f: FnSpec<(T, TreePath<N>), bool>, )

requires
Self::new_val(val, lv).inv(),
f(val, path),
ensures
Self::new_val(val, lv).subtree_satisfies(path, f),

If f(val, path), then TreeNode::new_val(val,lv).subtree_satisifies(path,f).

Source

pub proof fn lemma_subtree_satisfies_implies_and( self, path: TreePath<N>, f1: FnSpec<(T, TreePath<N>), bool>, f2: FnSpec<(T, TreePath<N>), bool>, g: FnSpec<(T, TreePath<N>), bool>, )

requires
self.inv(),
Self::implies(|v: T, p: TreePath<N>| f1(v, p) && f2(v, p), g),
Self::subtree_satisfies(self, path, f1),
Self::subtree_satisfies(self, path, f2),
ensures
Self::subtree_satisfies(self, path, g),

Proves subtree_satisfies(self, path, g) from two source predicates f1, f2, and the implication forall |v, p| v.inv() && f1(v, p) && f2(v, p) ==> g(v, p).

Source

pub proof fn tracked_new_val(tracked val: T, lv: nat) -> tracked res : Self

requires
0 <= lv < L,
N > 0,
val.inv(),
ensures
res.inv(),
returns
Self::new_val(val, lv),
Source

pub proof fn lemma_new_default_preserves_inv(lv: nat)

requires
0 <= lv < L,
N > 0,
forall |i: int| 0 <= i < N ==> #[trigger] T::default(lv).rel_children(i, None),
ensures
Self::new_default(lv).inv(),
Source

pub open spec fn insert(self, key: int, node: Self) -> Self

recommends
0 <= key < Self::size(),
node.level() == self.level() + 1,
{ Self::new(self.value(), self.level(), self.children().update(key, Some(node))) }

Insert the child at the given index.

Source

pub broadcast proof fn lemma_insert_preserves_inv(self, key: int, node: Self)

requires
self.inv(),
node.inv(),
node.level() == self.level() + 1,
self.value().rel_children(key, Some(node.value())),
ensures
self.insert(key, node).inv(),
Source

pub broadcast proof fn lemma_insert_property(self, key: int, node: Self)

requires
0 <= key < Self::size(),
self.inv(),
ensures
self.insert(key, node).value() == self.value(),
self.insert(key, node).children()[key] == Some(node),
self.insert(key, node).children() == self.children().update(key, Some(node)),
Source

pub proof fn lemma_insert_same_child_identical(self, key: int, node: Self)

requires
0 <= key < Self::size(),
self.inv(),
self.has_child(key),
self.child(key) == node,
ensures
self.insert(key, node) == self,
Source

pub open spec fn remove(self, key: int) -> Self

recommends
0 <= key < Self::size(),
{ Self::new(self.value(), self.level(), self.children().update(key, None)) }
Source

pub broadcast proof fn lemma_remove_preserves_inv(self, key: int)

requires
0 <= key < Self::size(),
self.inv(),
self.children()[key] is None || self.value().rel_children(key, None),
ensures
(#[trigger] self.remove(key)).inv(),
Source

pub broadcast proof fn lemma_remove_property(self, key: int)

requires
0 <= key < Self::size(),
self.inv(),
ensures
self.remove(key).value() == self.value(),
self.remove(key).children()[key] is None,
self.remove(key).children() == self.children().update(key, None),
Source

pub proof fn lemma_insert_child_is_child(self, key: int, node: Self)

requires
0 <= key < Self::size(),
self.inv(),
node.inv(),
self.level() < L - 1,
node.level() == self.level() + 1,
ensures
self.insert(key, node).has_child(key),
self.insert(key, node).child(key) == node,
Source

pub proof fn lemma_remove_child_is_none(self, key: int)

requires
0 <= key < Self::size(),
self.inv(),
ensures
!self.remove(key).has_child(key),
Source

pub open spec fn set_value(self, value: T) -> Self

recommends
self.inv(),
value.inv(),
{ Self::new(value, self.level(), self.children()) }
Source

pub broadcast proof fn lemma_set_value_observable_fields(self, value: T)

ensures
(#[trigger] self.set_value(value)).value() == value,
self.set_value(value).level() == self.level(),
self.set_value(value).children() == self.children(),

Exposes the observable fields changed and preserved by set_value.

Source

pub proof fn lemma_set_value_preserves_new_val_shape(self, value: T)

requires
self == Self::new_val(self.value(), self.level()),
ensures
self.set_value(value) == Self::new_val(value, self.level()),

Replacing the value of a childless node preserves its new_val shape.

Source

pub open spec fn is_leaf(self) -> bool

{ forall |i: int| 0 <= i < Self::size() ==> !#[trigger] self.has_child(i) }
Source

pub broadcast proof fn lemma_is_leaf_bounded(self)

requires
self.inv(),
self.level() == L - 1,
ensures
#[trigger] self.is_leaf(),
Source

pub open spec fn recursive_insert(self, path: TreePath<N>, node: Self) -> Self

recommends
self.inv(),
path.inv(),
path.len() < L - self.level(),
node.level() == self.level() + path.len() as nat,
{
    if path.is_empty() {
        self
    } else if path.len() == 1 {
        self.insert(path[0], node)
    } else {
        let (hd, tl) = path.pop_head();
        let child = if self.has_child(hd) {
            self.child(hd)
        } else {
            TreeNode::new_default(self.level() + 1)
        };
        let updated_child = child.recursive_insert(tl, node);
        self.insert(hd, updated_child)
    }
}
Source

pub proof fn lemma_recursive_insert_path_empty_identical( self, path: TreePath<N>, node: Self, )

requires
self.inv(),
node.inv(),
path.inv(),
path.is_empty(),
ensures
self.recursive_insert(path, node) == self,
Source

pub proof fn lemma_recursive_insert_path_len_1(self, path: TreePath<N>, node: Self)

requires
self.inv(),
node.inv(),
path.inv(),
path.len() == 1,
1 < L - self.level(),
node.level() == self.level() + 1,
ensures
self.recursive_insert(path, node) == self.insert(path[0], node),
Source

pub proof fn lemma_recursive_insert_path_len_step(self, path: TreePath<N>, node: Self)

requires
self.inv(),
path.inv(),
node.inv(),
path.len() < L - self.level(),
node.level() == self.level() + path.len() as nat,
path.len() > 1,
ensures
self.has_child(path[0])
    ==> self.recursive_insert(path, node)
        == self
            .insert(
                path[0],
                self.child(path[0]).recursive_insert(path.pop_head().1, node),
            ),
!self.has_child(path[0])
    ==> self.recursive_insert(path, node)
        == self
            .insert(
                path[0],
                TreeNode::new_default(self.level() + 1)
                    .recursive_insert(path.pop_head().1, node),
            ),
Source

pub proof fn lemma_recursive_insert_preserves_level( self, path: TreePath<N>, node: Self, )

requires
self.inv(),
path.inv(),
node.inv(),
path.len() < L - self.level(),
node.level() == self.level() + path.len() as nat,
forall |lv: nat| {
    lv < L ==> #[trigger] T::default(lv).rel_children(path.pop_tail().0 as int, None)
},
ensures
self.recursive_insert(path, node).level() == self.level(),
Source

pub proof fn lemma_recursive_insert_preserves_value( self, path: TreePath<N>, node: Self, )

requires
self.inv(),
path.inv(),
node.inv(),
path.len() < L - self.level(),
node.level() == self.level() + path.len() as nat,
forall |lv: nat, i: int| {
    lv < L && 0 <= i < N ==> #[trigger] T::default(lv).rel_children(i, None)
},
ensures
self.recursive_insert(path, node).value() == self.value(),
Source

pub proof fn lemma_recursive_insert_preserves_inv(self, path: TreePath<N>, node: Self)

requires
self.inv(),
path.inv(),
node.inv(),
path.len() < L - self.level(),
node.level() == self.level() + path.len() as nat,
self.recursive_seek(path.pop_tail().1) is Some
    ==> self.recursive_seek(path.pop_tail().1)->0
        .value()
        .rel_children(path.pop_tail().0 as int, Some(node.value())),
self.recursive_seek(path.pop_tail().1) is None
    ==> T::default((node.level() - 1) as nat)
        .rel_children(path.pop_tail().0 as int, Some(node.value())),
forall |lv: nat, i: int| {
    lv < L ==> (0 <= i < N ==> #[trigger] T::default(lv).rel_children(i, None))
},
ensures
self.recursive_insert(path, node).inv(),
Source

pub open spec fn recursive_trace(self, path: TreePath<N>) -> Seq<T>

recommends
self.inv(),
path.inv(),
path.len() < L - self.level(),
{
    if path.is_empty() {
        seq![self.value()]
    } else {
        let (hd, tl) = path.pop_head();
        if self.has_child(hd) {
            seq![self.value()].add(self.child(hd).recursive_trace(tl))
        } else {
            seq![self.value()]
        }
    }
}

Visit the tree node recursively based on the path Returns a sequence of visited node values, including the initial one If the path does not correspond to a node, stop the traverse, and return the previously visited nodes.

Source

pub proof fn lemma_recursive_trace_length(self, path: TreePath<N>)

requires
self.inv(),
path.inv(),
ensures
#[trigger] self.recursive_trace(path).len() <= path.len() + 1,
Source

pub proof fn lemma_recursive_trace_up_to( self, path1: TreePath<N>, path2: TreePath<N>, n: int, )

requires
self.inv(),
path1.inv(),
path2.inv(),
n <= path1.len(),
n <= path2.len(),
forall |i: int| 0 <= i < n ==> path1.0[i] == path2.0[i],
self.recursive_trace(path1).len() > n,
ensures
self.recursive_trace(path2).len() > n,
forall |i: int| {
    0 <= i <= n ==> self.recursive_trace(path1)[i] == self.recursive_trace(path2)[i]
},
Source

pub open spec fn recursive_seek(self, path: TreePath<N>) -> Option<Self>

recommends
self.inv(),
path.inv(),
path.len() < L - self.level(),
{
    if path.is_empty() {
        Some(self)
    } else {
        let (hd, tl) = path.pop_head();
        if self.has_child(hd) { self.child(hd).recursive_seek(tl) } else { None }
    }
}

Walk to the end of a path and return the subtree at the end Returns a single node (with its children) If the path does not correspond to a node, return None

Source

pub proof fn lemma_recursive_seek_trace_length(self, path: TreePath<N>)

requires
self.inv(),
path.inv(),
path.len() < L - self.level(),
self.recursive_seek(path) is Some,
ensures
self.recursive_trace(path).len() == path.len() + 1,
Source

pub proof fn lemma_recursive_seek_trace_next(self, path: TreePath<N>, idx: usize)

requires
self.recursive_seek(path) is Some,
self.recursive_seek(path)->0.has_child(idx as int),
self.inv(),
path.inv(),
path.len() < L - self.level(),
0 <= idx < N,
ensures
self.recursive_trace(path.push_tail(idx as int)).len() == path.len() + 2,
self.recursive_seek(path)->0.child(idx as int).value()
    == self.recursive_trace(path.push_tail(idx as int))[path.len() as int + 1],
Source

pub open spec fn recursive_visit(self, path: TreePath<N>) -> Seq<Self>

recommends
self.inv(),
path.inv(),
path.len() < L - self.level(),
{
    if path.is_empty() {
        Seq::empty()
    } else if path.len() == 1 {
        if self.has_child(path[0]) { seq![self.child(path[0])] } else { Seq::empty() }
    } else {
        let (hd, tl) = path.pop_head();
        if self.has_child(hd) {
            let child = self.child(hd);
            seq![child].add(child.recursive_visit(tl))
        } else {
            Seq::empty()
        }
    }
}

Visit the tree node recursively based on the path Returns a sequence of visited nodes, exclude the given one If the path is empty, return an empty sequence If the tree node is absent, stop the traverse, and return the previously visited nodes.

Source

pub proof fn lemma_recursive_visited_node_inv(self, path: TreePath<N>)

requires
self.inv(),
path.inv(),
path.len() < L - self.level(),
ensures
forall |i: int| {
    0 <= i < self.recursive_visit(path).len() ==> #[trigger]
        self.recursive_visit(path)[i].inv()
},
Source

pub proof fn lemma_recursive_visited_node_levels(self, path: TreePath<N>)

requires
self.inv(),
path.inv(),
path.len() < L - self.level(),
ensures
forall |i: int| {
    0 <= i < self.recursive_visit(path).len()
        ==> #[trigger] self.recursive_visit(path)[i].level() == self.level() + i + 1
},
Source

pub proof fn lemma_recursive_visit_head(self, path: TreePath<N>)

requires
self.inv(),
path.inv(),
path.len() < L - self.level(),
!path.is_empty(),
self.recursive_visit(path).len() > 0,
ensures
self.recursive_visit(path)[0] == self.child(path[0]),
Source

pub proof fn lemma_recursive_visit_induction(self, path: TreePath<N>)

requires
self.inv(),
path.inv(),
path.len() < L - self.level(),
!path.is_empty(),
self.recursive_visit(path).len() > 0,
ensures
self.recursive_visit(path)
    == seq![self.child(path.pop_head().0)]
        .add(self.child(path.pop_head().0).recursive_visit(path.pop_head().1)),
Source

pub proof fn lemma_recursive_visit_one_is_child(self, path: TreePath<N>)

requires
self.inv(),
path.inv(),
path.len() < L - self.level(),
path.len() == 1,
ensures
self.has_child(path[0]) ==> self.recursive_visit(path) == seq![self.child(path[0])],
!self.has_child(path[0]) ==> self.recursive_visit(path) == seq![],
Source

pub open spec fn on_subtree(self, node: Self) -> bool

recommends
self.inv(),
node.inv(),
node.level() >= self.level(),
node.level() < L,
{
    node == self
        || exists |path: TreePath<N>| {
            #[trigger] path.inv() && path.len() > 0
                && path.len() == node.level() - self.level()
                && self.recursive_visit(path).last() == node
        }
}
Source

pub broadcast proof fn lemma_on_subtree_property(self, node: Self)

requires
self.inv(),
node.inv(),
node.level() >= self.level(),
node.level() < L,
#[trigger] self.on_subtree(node),
ensures
node.level() == self.level() ==> self == node,
node.level() > self.level()
    ==> exists |path: TreePath<N>| {
        #[trigger] path.inv() && path.len() == node.level() - self.level()
            && self.recursive_visit(path).last() == node
    },
Source

pub broadcast proof fn lemma_not_on_subtree_property(self, node: Self)

requires
self.inv(),
node.inv(),
node.level() < L,
!#[trigger] self.on_subtree(node),
ensures
self != node,
node.level() > self.level()
    ==> forall |path: TreePath<N>| {
        #[trigger] path.inv() && path.len() == node.level() - self.level()
            ==> self.recursive_visit(path).last() != node
    },
Source

pub broadcast proof fn lemma_on_subtree_reflexive(self)

requires
self.inv(),
ensures
#[trigger] self.on_subtree(self),
Source

pub broadcast proof fn lemma_child_on_subtree(self, key: int)

requires
0 <= key < Self::size(),
self.inv(),
self.has_child(key),
ensures
#[trigger] self.on_subtree(self.child(key)),
Source

pub broadcast proof fn lemma_insert_on_subtree(self, key: int, node: Self)

requires
0 <= key < Self::size(),
self.inv(),
node.inv(),
self.level() < L - 1,
node.level() == self.level() + 1,
self.value().rel_children(key, Some(node.value())),
ensures
#[trigger] self.insert(key, node).on_subtree(node),
Source

pub open spec fn recursive_remove(self, path: TreePath<N>) -> Self

recommends
self.inv(),
path.inv(),
path.len() < L - self.level(),
{
    if path.is_empty() {
        self
    } else if path.len() == 1 {
        self.remove(path[0])
    } else {
        let (hd, tl) = path.pop_head();
        if self.children()[hd as int] is None {
            self
        } else {
            let child = self.child(hd);
            let updated_child = child.recursive_remove(tl);
            self.insert(hd, updated_child)
        }
    }
}

Remove the tree node at the end of the path If the path is empty or any node in the path is absent, return the original tree node (no change) Otherwise, remove the node at the end of the path, and update the node recursively

Source

pub proof fn lemma_recursive_remove_preserves_level(self, path: TreePath<N>)

requires
self.inv(),
path.inv(),
path.len() < L - self.level(),
ensures
self.recursive_remove(path).level() == self.level(),
Source

pub proof fn lemma_recursive_remove_preserves_value(self, path: TreePath<N>)

requires
self.inv(),
path.inv(),
path.len() < L - self.level(),
ensures
self.recursive_remove(path).value() == self.value(),
Source

pub proof fn lemma_recursive_remove_preserves_inv(self, path: TreePath<N>)

requires
self.inv(),
path.inv(),
path.len() < L - self.level(),
path.len() > 0
    ==> (self.recursive_seek(path.pop_tail().1) is Some
        ==> self.recursive_seek(path.pop_tail().1)->0
            .children()[path.pop_tail().0 as int] is None
            || self.recursive_seek(path.pop_tail().1)->0
                .value()
                .rel_children(path.pop_tail().0 as int, None)),
ensures
self.recursive_remove(path).inv(),

Auto Trait Implementations§

§

impl<T, const N: usize, const L: usize> Freeze for TreeNode<T, N, L>
where T: Freeze,

§

impl<T, const N: usize, const L: usize> RefUnwindSafe for TreeNode<T, N, L>
where T: RefUnwindSafe,

§

impl<T, const N: usize, const L: usize> Send for TreeNode<T, N, L>
where T: Send,

§

impl<T, const N: usize, const L: usize> Sync for TreeNode<T, N, L>
where T: Sync,

§

impl<T, const N: usize, const L: usize> Unpin for TreeNode<T, N, L>
where T: Unpin,

§

impl<T, const N: usize, const L: usize> UnsafeUnpin for TreeNode<T, N, L>
where T: UnsafeUnpin,

§

impl<T, const N: usize, const L: usize> UnwindSafe for TreeNode<T, N, L>
where T: UnwindSafe,

Blanket Implementations§

Source§

impl<T> Any for T
where T: 'static + ?Sized,

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

impl<T> Borrow<T> for T
where T: ?Sized,

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

Source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
Source§

impl<T> From<T> for T

Source§

fn from(t: T) -> T

Returns the argument unchanged.

§

impl<T, VERUS_SPEC__A> FromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: From<T>,

§

fn obeys_from_spec() -> bool

§

fn from_spec(v: T) -> VERUS_SPEC__A

Source§

impl<T, U> Into<U> for T
where U: From<T>,

Source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

§

impl<T, VERUS_SPEC__A> IntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: Into<T>,

§

fn obeys_into_spec() -> bool

§

fn into_spec(self) -> T

§

impl<T, U> IntoSpecImpl<U> for T
where U: From<T>,

§

fn obeys_into_spec() -> bool

§

fn into_spec(self) -> U

Source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
§

impl<T, VERUS_SPEC__A> TryFromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryFrom<T>,

§

fn obeys_try_from_spec() -> bool

§

fn try_from_spec( v: T, ) -> Result<VERUS_SPEC__A, <VERUS_SPEC__A as TryFrom<T>>::Error>

Source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.
§

impl<T, VERUS_SPEC__A> TryIntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryInto<T>,

§

fn obeys_try_into_spec() -> bool

§

fn try_into_spec(self) -> Result<T, <VERUS_SPEC__A as TryInto<T>>::Error>

§

impl<T, U> TryIntoSpecImpl<U> for T
where U: TryFrom<T>,

§

fn obeys_try_into_spec() -> bool

§

fn try_into_spec(self) -> Result<U, <U as TryFrom<T>>::Error>

§

impl<A> SpecEq<&A> for A
where A: ?Sized,

§

impl<A> SpecEq<&mut A> for A
where A: ?Sized,

§

impl<A> SpecEq<A> for A
where A: ?Sized,

§

impl<A> SpecEq<Ghost<A>> for A

§

impl<A> SpecEq<Tracked<A>> for A