Delay monad interface and model

[Ryuji-Kawakami]

We define the delay monad interface and prove the soundness of it. Additionally, we construct the model of combination with state monad and exception monad.
And we turned the typed store monad into a monad transformer as a composition of state monad transformer and exception monad transformer.

[affeldt-aist]

It would be nice if you could keep the examples about the delay monad in one file and the models about the delay monad in one file (this is to ease long-term maintenance).
It would also be nice if you could restore blank lines between Qed. and Lemma .../Definition .... (it is easier to read and is less likely to cause errors when processing with documentation tools.)

[affeldt-aist]

Use - instead of ** (this breaks the indentation pattern of two characters otherwise)

[affeldt-aist]

Comments will need to be removed when you moved from draft to PR.
Also, files deserve some documentation (look at other files for examples).

[affeldt-aist]

This is a great addition and I understand that this is still in draft mode.
I wrote a few style-level comments that I think could help clarify the presentation of the code.
Rebase on top of master (that has moved from MathComp 2.2.0 to 2.3.0 is also needed,
we gave up on 2.2.0).

[affeldt-aist]

Rebase on top of master (that has moved from MathComp 2.2.0 to 2.3.0 is also needed, we gave up on 2.2.0).

Rebasing on top top of master and using MathComp 2.3.0 should get rid at least of one CI error.

[affeldt-aist]

This code, as well as other code below, is already present in example_typed_store.v. Could you come up with a way to share this code to avoid copy-pasting? (This is important for maintenance and this can only clarify your work.)

[affeldt-aist]

This file (other files as well) should come with a (short) comment at the top that explains what this file is about, in this case, answering the question, "what's the relation with typed_store_model.v?".