Trait creusot_contracts::logic::ops::IndexLogic

pub trait IndexLogic<I: ?Sized> {
    type Item;

    // Required method
    fn index_logic(self, idx: I) -> Self::Item;
}

Used for indexing operations (container[index]) in pearlite.

Required Associated Types

type Item

Required Methods

fn index_logic(self, idx: I) -> Self::Item

Performs the indexing (container[index]) operation.

logic

Implementations on Foreign Types

impl<T> IndexLogic<usize> for [T]

fn index_logic(self, ix: usize) -> Self::Item

logic

pearlite! { self@[ix@] }

type Item = T

impl<T> IndexLogic<Int> for [T]

fn index_logic(self, ix: Int) -> Self::Item

logic

pearlite! { self@[ix] }

type Item = T

impl<T, const N: usize> IndexLogic<usize> for [T; N]

fn index_logic(self, ix: usize) -> Self::Item

logic

pearlite! { self@[ix@] }

type Item = T

impl<T, const N: usize> IndexLogic<Int> for [T; N]

fn index_logic(self, ix: Int) -> Self::Item

logic

pearlite! { self@[ix] }

type Item = T

Implementors

impl<A: ?Sized, B> IndexLogic<A> for Mapping<A, B>

type Item = B

impl<K, V> IndexLogic<K> for FMap<K, V>

type Item = V

impl<T> IndexLogic<Int> for Snapshot<Seq<T>>

type Item = T

impl<T> IndexLogic<Int> for Seq<T>

type Item = T

impl<T, A: Allocator> IndexLogic<usize> for VecDeque<T, A>

type Item = T

impl<T, A: Allocator> IndexLogic<usize> for Vec<T, A>

type Item = T

impl<T, A: Allocator> IndexLogic<Int> for VecDeque<T, A>

type Item = T

impl<T, A: Allocator> IndexLogic<Int> for Vec<T, A>

type Item = T