Email Gateway (Mar 13 2023 at 14:27): Email Gateway (Mar 13 2023 at 14:27):From: Peter Lammich <lammich@in.tum.de>
"i_hate_words"! Seriously?
This lemma name just came up on sledgehammer ... and it's apparently
also used by other AFP-Entries:
Email Gateway (Mar 13 2023 at 14:55):From: Peter Lammich <lammich@in.tum.de>
btw:
lemmas [no_atp] = i_hate_words i_hate_words_helper
effectively stops the (automated) spread of hate speech ;)
Email Gateway (Mar 13 2023 at 14:59):From: Thomas Sewell <tals4@cam.ac.uk>
The i_hate_words name sounds like it might be my fault. Dealing with words/bitvectors in any logic seems to be a nuisance, but dealing with early versions of the word library was particularly unpleasant. There were quite a few asides in the L4.verified project that used, erm, obvious stand-ins for more inappropriate language, most of which were removed prior to it all being open-sourced. Looks like that one survived.
It probably wouldn't have occured to any of us, at the time, that the sledgehammer might dredge up some of these internal names in the future. They should probably just be replaced.
Best regards,
Thomas.
Email Gateway (Mar 13 2023 at 15:02):From: Peter Lammich <lammich@in.tum.de>
That shed's some nice light onto the history of the Word-Lib (or any
other developments from first prototypes, to discovering concepts, to
making it a mature library).
In its current state, I find it really convenient to use :)
Last updated: Jan 04 2025 at 20:18 UTC