Sage Binder (Nov 05 2024 at 01:05): Sage Binder (Nov 05 2024 at 01:05):Hello,
I have just finished formalizing some results which I would like to submit to the AFP soon. The results involve the Jordan Normal Form library. Due to conflicting definition names, I have had to hide many definitions from the old matrix library (I needed to hide around 30 to 40 definitions total, that is, 15 to 20 hide_fact/hide_const pairs):
hide_type (open) Matrix_Legacy.mat
hide_const (open) Matrix_Legacy.mat
hide_fact (open) Finite_Cartesian_Product.mat_def
hide_const (open) Finite_Cartesian_Product.mat
hide_fact (open) Matrix_Legacy.mat_def
hide_const (open) Finite_Cartesian_Product.row
hide_fact (open) Finite_Cartesian_Product.row_def
hide_const (open) Matrix_Legacy.row
hide_fact (open) Matrix_Legacy.row_def
hide_const (open) Matrix_Legacy.col
hide_fact (open) Matrix_Legacy.col_def
hide_const (open) Determinants.det
hide_fact (open) Determinants.det_def
...
Is it acceptable for an AFP entry to begin this way, with hiding many facts and constants? Also, is it important that I include "(open)" in all hidden facts/consts so that theories which import this entry may still use things that have been hidden?
Thank you
Yong Kiam (Nov 05 2024 at 01:59):I would recommend emailing the AFP editors to ask directly (and let us know the answer here)
Mathias Fleury (Nov 05 2024 at 05:41):Side remark, you can put several theorems in a line:
hide_fact (open) TrueI ATP.fTrue_def
Just an update to this:
I did not hear back from the AFP editors, so I decided to just submit with a comment asking about this. The entry (Two Theorems on Hermitian Matrices) was accepted to the AFP as-is, so I suppose it’s not a problem.
Last updated: Dec 21 2024 at 16:20 UTC