Struct Mapping 

pub struct Mapping<A: ?Sized, B>(/* 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> Mapping<A, B>

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

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

pub fn ext_eq(self, x: Self) -> bool

Extensional equality.

Returns true if self and other contain exactly the same key-value pairs.

This is in fact equivalent with normal equality.

logic

Trait Implementations

impl<T> GuardRef<T> for Mapping<T, bool>

fn guards_ref(self, x: T) -> bool

logic(open, inline)

self[x]

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

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

logic(open, inline)

self.get(a)

type Item = B