Snippets Groups Projects

Commit 9c1d9abd authored 3 years ago by Jacques-Henri Jourdan

The introduction pattern \!# is deprecated. Replace by \!>.

parent 75f6aaae

No related branches found

No related tags found

Checking pipeline status

Hide whitespace changes

Inline Side-by-side

Showing with 97 additions and 97 deletions

Ralf Jung @jung · 3 years ago

Owner

Ah, I also keep using !# accidentally in new code... given that # stands for "intuitionistic context", it just makes way too much sense.

@robbertkrebbers I am honestly wondering if we should take back that deprecation. We also still have iNext, so why not also still have !# which can only introduce the persistently modality?

Ah, I also keep using `!#` accidentally in new code... given that `#` stands for "intuitionistic context", it just makes way too much sense. @robbertkrebbers I am honestly wondering if we should take back that deprecation. We also still have `iNext`, so why not also still have `!#` which can only introduce the persistently modality?

Please register or to comment