Irvin
Irvin
It seems to fail when the theorem is actually used. If you modify `PAIR_MAP_I` in pairTheory, it fails when it's seems to be used by the quotient library in resulting...
I been wondering whether contexts can be emulated with PolyML.NameSpaces
The plan would only store the list theorems used to simplify . so that you simplify with a pure_simp_tac variant
I was thinking it would be more simp[] to asm_simp_tac(pure_ss)[..] but i'm not sure whether @myreen or @digama0 thinks the same.
The maintainability comes from that new simp rules won't break old proofs.
Note that it only seems to appear for interactive mode. Building a theory and having it depend on bug with the check removed there's only one cong. I suspect that...
I also think that its fine for it to do the calculate key, `lookup cache .. ` steps when an ancestor is changed without its dat changing. It will cache...
The main thing is that different keys can point to the same build output.
I don't think following nix is the way to go. Nix has to be too conservative due to it working as a general build system. For example in nix a...
Anything less than comparing based on build output is being conservative. Comments are just one feature that a generic hash all sources will not be able to detect. I personally...