Comprehensive Documentation of Contract Usage

[JustusAdam]

There should be an example driven documentation of how contracts are to be used that we can link to from e.g. the requires, ensures, stub_verified, proof_for_contract attribute documentation.

[pi314mm]

Also documentation for old for history expressions