As arch-split of Refine proceeded, we ended up with a confusing situation. We had to do crunches over Arch.blah functions, which resulted in confusion for crunch and generation of funky names. Then we decided that in cases where this happens a bunch for the same constant, adding an Arch_blah input abbreviation would help get more sane names. This worked, but now it made sense for the lemma name for Arch_blah to also be named Arch_blah_....
Now having completed the first pass of arch-splitting Refine we learned the following:
- we don't like lemmas starting with capital letters, so at minimum these should be with a lowercase
a in the interface assumptions
- it does not make practical sense to keep spelling out which parts of the crunch we specifically want to point out are used to satisfy Arch interface assumptions;
for ....[Whatever_assms] is sufficient, meaning the actual name of the lemma doesn't matter that much; the lemma will get a proper name when the interface is interpreted/instantiated
Therefore:
assumes Arch_ should become assumes arch_- the
lemmas [Whatever_assms] directly after a crunch should be reviewed and folded into the crunch unless something exceptional is going on
As arch-split of Refine proceeded, we ended up with a confusing situation. We had to do crunches over
Arch.blahfunctions, which resulted in confusion for crunch and generation of funky names. Then we decided that in cases where this happens a bunch for the same constant, adding anArch_blahinput abbreviation would help get more sane names. This worked, but now it made sense for the lemma name forArch_blahto also be namedArch_blah_....Now having completed the first pass of arch-splitting Refine we learned the following:
ain the interface assumptionsfor ....[Whatever_assms]is sufficient, meaning the actual name of the lemma doesn't matter that much; the lemma will get a proper name when the interface is interpreted/instantiatedTherefore:
assumes Arch_should becomeassumes arch_lemmas [Whatever_assms]directly after a crunch should be reviewed and folded into the crunch unless something exceptional is going on