[Iris-Club] Frame-preserving update and double-negation

Ralf Jung jung at mpi-sws.org
Wed Aug 24 21:04:48 CEST 2016


Hi,

>> That's cute.  We should put this somewhere in the repo.  Could you put
>> it into some file (algebra/double_negation or so?)
> If you want to keep track of such facts in the Iris repository, I would
> be in favor of putting them in an additional folder, together with
> things like program_logic/counter_examples.v.
> 
> Any suggestions for an appropriate name for this folder?

base_logic/facts/ (following the new folder layout)?

Kind regards,
Ralf




More information about the Iris-Club mailing list