[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