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::fset::FSet;

pub use self::ord::OrdLogic;

pub use self::seq::Seq;

Modules

fset

ops

ord

Definition for using orderings in pearlite.

ra

Definitions of Resource Algebras

real

Real numbers

seq

Structs

FMap

A finite map 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.

Set

A (possibly infinite) set type.

Traits

WellFounded

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

Functions

such_that

Creates a logical value satisfying the property given by p.

unreachable

Indicates unreachable code in logic.