Module invariant 

Type invariants

See Invariant.

Structs

Guarded

A borrow guarded by an invariant.

Subset

A subset type.

Traits

InhabitedInvariant

A type implements InhabitedInvariant when its type invariant is inhabited. This is needed to define subset types.

Invariant

A user-defined type invariant.

Functions

inv

Whether the invariant of a value holds

Type Aliases

GuardedBorrow

A mutable borrow, that asserts an invariant called the guard.