Module invariant 

Type invariants

See Invariant.

Structs

Guarded

Guarded is a wrapper around an object of type T, which makes sure that a guard (a predicate on T) is satisfied when the guarded object disappears. It works by making the guard part of the type invariant of Guarded, and uses some internal Creusot machinery to ensure that the guard never changes during the lifetime of the Guarded object.

IsSome

Guard an Option that must remain Some.

Subset

A subset type.

Traits

Guard

Guards that can be used in Guarded.

GuardRef

Guard predicate under mutable references.

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