Node

vstd_extra::ghost_tree

Struct Node 

Source 
pub struct Node<T: TreeNodeValue<L>, const N: usize, const L: usize> {
    pub value: T,
    pub level: nat,
    pub children: Seq<Option<Node<T, N, L>>>,
}
Expand description

A ghost tree node with maximum N children, the maximum depth of the tree is L Each tree node has a value of type T and a sequence of children

Fields§

§value: T§level: nat§children: Seq<Option<Node<T, N, L>>>

Implementations§

Source§

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

Source

pub open spec fn size() -> nat

{ N as nat }
Source

pub open spec fn max_depth() -> nat

{ L as nat }
Source

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

ensures
*res == self.value,
Source

pub proof fn axiom_size_positive()

ensures
Self::size() > 0,
Source

pub proof fn axiom_max_depth_positive()

ensures
Self::max_depth() > 0,
Source

pub open spec fn tree_predicate_map( 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.children[i] is Some
                    ==> self.children[i]->Some_0
                        .tree_predicate_map(path.push_tail(i as usize), f))
        }

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

    }
}
Source

pub proof fn map_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.children[i] is Some,
self.tree_predicate_map(path, f),
ensures
self.children[i]->Some_0.tree_predicate_map(path.push_tail(i as usize), 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 map_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::tree_predicate_map(self, path, f),
ensures
Self::tree_predicate_map(self, path, g),
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

{
    &&& 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 open spec fn new(lv: nat) -> Self

{
    Node {
        value: T::default(lv),
        level: lv,
        children: Seq::new(N as nat, |i| None),
    }
}
Source

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

recommends
lv < L,
{
    Node {
        value: val,
        level: lv,
        children: Seq::new(N as nat, |i| Some(Self::new(lv + 1))),
    }
}
Source

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

requires
lv < L,
ensures
res.inv(),
Source

pub broadcast proof fn new_preserves_inv(lv: nat)

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

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

recommends
0 <= key < Self::size(),
self.inv(),
node.inv(),
self.level < L - 1,
node.level == self.level + 1,
{
    Node {
        children: self.children.update(key as int, Some(node)),
        ..self
    }
}
Source

pub broadcast proof fn insert_preserves_inv(self, key: usize, 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 as int, Some(node.value)),
ensures
#[trigger] self.insert(key, node).inv(),
Source

pub broadcast proof fn insert_property(self, key: usize, node: Self)

requires
0 <= key < Self::size(),
self.inv(),
node.inv(),
self.level < L - 1,
node.level == self.level + 1,
ensures
#[trigger] self.insert(key, node).value == self.value,
self.insert(key, node).children[key as int] == Some(node),
forall |i: int| {
    0 <= i < Self::size() && i != key
        ==> #[trigger] self.insert(key, node).children[i] == self.children[i]
},
Source

pub broadcast proof fn insert_same_child_identical(self, key: usize, node: Self)

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

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

recommends
0 <= key < Self::size(),
self.inv(),
{
    Node {
        children: self.children.update(key as int, None),
        ..self
    }
}
Source

pub broadcast proof fn remove_preserves_inv(self, key: usize)

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

pub broadcast proof fn remove_property(self, key: usize)

requires
0 <= key < Self::size(),
self.inv(),
ensures
#[trigger] self.remove(key).value == self.value,
self.remove(key).children[key as int] is None,
forall |i: int| {
    0 <= i < Self::size() && i != key
        ==> #[trigger] self.remove(key).children[i] == self.children[i]
},
Source

pub open spec fn child(self, key: usize) -> Option<Self>

recommends
0 <= key < Self::size(),
self.inv(),
{ self.children[key as int] }
Source

pub proof fn tracked_child(self, key: usize) -> res : Option<Self>

requires
0 <= key < Self::size(),
ensures
res == self.child(key),
Source

pub broadcast proof fn child_property(self, key: usize)

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

pub broadcast proof fn child_property_cases(self, key: usize)

requires
0 <= key < Self::size(),
self.inv(),
ensures
self.level == L - 1 ==> #[trigger] self.child(key) is None,
self.level < L - 1 && self.children[key as int] is None ==> #[trigger]
    self.child(key) is None,
self.level < L - 1 && self.children[key as int] is Some
    ==> #[trigger] self.child(key) is Some
        && self.child(key)->Some_0.level == self.level + 1
        && self.child(key)->Some_0.inv(),
Source

pub proof fn child_some_properties(self, key: usize)

requires
0 <= key < Self::size(),
self.inv(),
self.child(key) is Some,
ensures
self.level < L - 1,
self.child(key)->Some_0.level == self.level + 1,
self.child(key)->Some_0.inv(),
Source

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

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

pub broadcast proof fn lemma_remove_child_is_none(self, key: usize)

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

pub open spec fn get_value(self) -> T

{ self.value }
Source

pub broadcast proof fn get_value_property(self)

requires
self.inv(),
ensures
#[trigger] self.get_value() == self.value,
self.get_value().inv(),
Source

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

recommends
self.inv(),
value.inv(),
{ Node { value: value, ..self } }
Source

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

requires
self.inv(),
value.inv(),
value.la_inv(self.level),
forall |i: int| {
    0 <= i < N
        ==> (#[trigger] self.children[i] is Some
            ==> value.rel_children(i, Some(self.children[i]->Some_0.value)))
},
forall |i: int| {
    0 <= i < N ==> (#[trigger] self.children[i] is None ==> value.rel_children(i, None))
},
ensures
#[trigger] self.set_value(value).value == value,
self.set_value(value).children == self.children,
self.set_value(value).inv(),
Source

pub open spec fn is_leaf(self) -> bool

{ forall |i: int| 0 <= i < Self::size() ==> self.children[i] is None }
Source

pub broadcast proof fn 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(),
node.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.index(0), node)
    } else {
        let (hd, tl) = path.pop_head();
        let child = match self.child(hd) {
            Some(child) => child,
            None => Node::new(self.level + 1),
        };
        let updated_child = child.recursive_insert(tl, node);
        self.insert(hd, updated_child)
    }
}
Source

pub broadcast 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
#[trigger] self.recursive_insert(path, node) == self,
Source

pub broadcast 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
#[trigger] self.recursive_insert(path, node) == self.insert(path.index(0), node),
Source

pub broadcast 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.child(path.index(0)) is Some
    ==> #[trigger] self.recursive_insert(path, node)
        == self
            .insert(
                path.index(0),
                self.child(path.index(0))->Some_0
                    .recursive_insert(path.pop_head().1, node),
            ),
self.child(path.index(0)) is None
    ==> #[trigger] self.recursive_insert(path, node)
        == self
            .insert(
                path.index(0),
                Node::new(self.level + 1).recursive_insert(path.pop_head().1, node),
            ),
Source

pub broadcast 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
#[trigger] self.recursive_insert(path, node).level == self.level,
Source

pub broadcast 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
#[trigger] self.recursive_insert(path, node).value == self.value,
Source

pub broadcast 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)->Some_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
#[trigger] 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();
        match self.child(hd) {
            Some(child) => seq![self.value].add(child.recursive_trace(tl)),
            None => 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();
        match self.child(hd) {
            Some(child) => child.recursive_seek(tl),
            None => 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)->Some_0.children[idx as int] is Some,
self.inv(),
path.inv(),
path.len() < L - self.level,
0 <= idx < N,
ensures
self.recursive_trace(path.push_tail(idx)).len() == path.len() + 2,
self.recursive_seek(path)->Some_0.children[idx as int]->Some_0.value
    == self.recursive_trace(path.push_tail(idx))[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 {
        match self.child(path.index(0)) {
            Some(child) => seq![child],
            None => Seq::empty(),
        }
    } else {
        let (hd, tl) = path.pop_head();
        match self.child(hd) {
            Some(child) => seq![child].add(child.recursive_visit(tl)),
            None => 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 broadcast proof fn lemma_recursive_visited_node_inv(self, path: TreePath<N>)

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

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

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

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

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

pub broadcast 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
#[trigger] self.recursive_visit(path)
    == seq![self.child(path.pop_head().0) -> Some_0,]
        .add(self.child(path.pop_head().0)->Some_0.recursive_visit(path.pop_head().1)),
Source

pub broadcast 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.child(path.index(0)) is Some
    ==> (#[trigger] self.recursive_visit(path)
        =~= seq![self.child(path.index(0)) -> Some_0,]),
self.child(path.index(0)) is None ==> (#[trigger] 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 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 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: usize)

requires
0 <= key < Self::size(),
self.inv(),
self.child(key) is Some,
ensures
#[trigger] self.on_subtree(self.child(key)->Some_0),
Source

pub broadcast proof fn lemma_insert_on_subtree(self, key: usize, 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 as int, 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.index(0))
    } else {
        let (hd, tl) = path.pop_head();
        if self.child(hd) is None {
            self
        } else {
            let child = self.child(hd)->Some_0;
            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 broadcast proof fn lemma_recursive_remove_preserves_level(self, path: TreePath<N>)

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

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

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

pub broadcast 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)->Some_0
            .children[path.pop_tail().0 as int] is None
            || self.recursive_seek(path.pop_tail().1)->Some_0
                .value
                .rel_children(path.pop_tail().0 as int, None)),
ensures
#[trigger] self.recursive_remove(path).inv(),

Auto Trait Implementations§

§

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

§

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

§

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

§

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

§

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

§

impl<T, const N: usize, const L: usize> UnwindSafe for Node<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>