Crate adhesion

This crate's formal documentation is under construction! The best documentation is currently found in the README.md and the resources it points to. The easiest way to find it is by looking through the repo here.

Macros

contract

Converts a fn definition inside to be a contracted function, complete with invariant, pre-, and post-conditions.