Struct creusot_contracts::logic::Mapping

pub struct Mapping<A: ?Sized, B: ?Sized>(/* private fields */);

A mapping: map every value of type A to a value of type B.

Pearlite syntax

Mappings have special support in pearlite code: you may write a closure to create a mapping.

Example

let value = snapshot!(4);
let map: Snapshot<Mapping<Int, Int>> = snapshot!(|n| if n % 2 == 0 { 0 } else { *value });
proof_assert!(map.get(1) == 4);

Implementations

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

pub fn get(self, a: A) -> B

where B: Sized,

Get the value associated with a in the map.

logic

pub fn set(self, a: A, b: B) -> Self

Returns a new mapping, where a is now mapped to b.

logic

pub fn cst(b: B) -> Self

Create a mapping, where every value of type a is mapped to b.

logic

Trait Implementations

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

fn index_logic(self, a: A) -> B

logic

self.get(a)

type Item = B