Module invariant 

Type invariants

Structs

Subset

A subset type.

Traits

InhabitedInvariant

A type implements InhabitedInvariants 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