[Iris-Club] Frame-preserving update and double-negation
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
More information about the Iris-Club