Commit 336a8c7d authored by Robbert Krebbers's avatar Robbert Krebbers

Tweak modalities doc.

parent 9b44e889
Pipeline #15015 passed with stage
in 10 minutes and 58 seconds
......@@ -8,8 +8,8 @@ instantiated with a variety of modalities.
For the purpose of MoSeL, a modality is a mapping of propositions
`M : PROP1 → PROP2` (where `PROP1` and `PROP2` are BI-algebras, although usually
it is the same algebra) that is monotone and distributes over finite products.
Specifically, the following rules have to be satisfied:
it is the same algebra) that is monotone and distributes over separating
conjunction. Specifically, the following rules have to be satisfied:
P ⊢ Q emp ⊢ M emp
----------
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment