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

Robbert Krebbers mail at robbertkrebbers.nl
Wed Aug 24 21:17:26 CEST 2016

On 08/24/2016 09:04 PM, Ralf Jung wrote:
>>> 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)?
Hmm, I would like the name of this folder to reflect that these 'facts' 
are not needed for the actual Iris logic, but are just there for 
informative purposes.

More information about the Iris-Club mailing list