Skip to content

rename affinely_persistently -> intuitionistically; and make it a TC-opaque definition

Ralf Jung requested to merge ralf/intuitionistically into gen_proofmode

I am very unsure about the instances in class_instances.v -- both about what I added (necessary to make it all compile again), and about what else I should add because the modality commutes with various things.

This will break reverse dependencies if they relied on "intuitionitsically" to be syntactically equal (and not just convertible) to "affinely persistently".

Fixes #126 (closed)

Edited by Ralf Jung

Merge request reports