Skip to content

Persistently: Get rid of mono and idemp in favor of intro

Ralf Jung requested to merge ralf/persistently into master

Turns out that intro is strong enough to derive both mono and idemp. I think having intro and elim primitive is neater; this also matches the usual presentation of ! in (intuitionistic) linear logic. If you agree, I can do the same for plainly.

Of course, I find this right after I tagged Iris 3.1.0.

Edited by Ralf Jung

Merge request reports