Module logic 

Definitions for pearlite code

This contains types and traits that are meant to be used in logical code.

Re-exports

pub use self::fmap::FMap;

pub use self::ord::OrdLogic;

pub use self::ord::PartialOrdLogic;

pub use self::seq::Seq;

Modules

fmap

A logical/ghost finite map.

ops

ord

Definition for using orderings in Pearlite.

ra

Definitions of Resource Algebras

real

Real numbers

seq

Structs

FSet

A finite set type usable in pearlite and ghost! blocks.

Id

A unique id, usable in logic and ghost code

Int

An unbounded, mathematical integer.

Mapping

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

Nat

Natural numbers, i.e., integers that are greater or equal to 0.

Positive

Positive numbers, i.e. numbers that are strictly greater than 0.

Set

A (possibly infinite) set type.

Traits

WellFounded

Instances of this trait are types which are allowed as variants of recursive definitions.

Functions

any

Return a logical value of type T without any constraints.

such_that

Creates a logical value satisfying the property given by p.

try_such_that

A variant of such_that that returns an Option<T>, returning None if no value satisfies the property.