<html><head><style type='text/css'>p { margin: 0; }</style></head><body><div style='font-family: times new roman,new york,times,serif; font-size: 12pt; color: #000000'><span style="font-family: arial; font-size: small; ">Hello,</span><div style="font-family: arial; font-size: small; "><br></div><div style="font-family: arial; font-size: small; ">I am working on a translation from OpenTheory to Dedukti (<a href="http://www.lix.polytechnique.fr/dedukti/" target="_blank">http://www.lix.polytechnique.<wbr>fr/dedukti/</a>), a proof system close to the LF and Coq family. I have some questions regarding the packaging of some theories in the standard library.</div><div style="font-family: arial; font-size: small; "><br></div><div style="font-family: arial; font-size: small; ">1. Our biggest obstacle right now is inductive type definitions. It turns out it is very expensive to type-check the complex machanisms of inductive type definitions the way they are currently implemented in HOL (and hence in OpenTheory). However, these mechanisms are hidden in the packages that use them (e.g. in list-def, option-def, sum-def) and therefore reappear in each of them, resulting in bloated packages. Is there any reason why inductive type definitions have not been formalized in a separate package, on which the theories using them (list, option, sum, etc.) depend on?</div><div style="font-family: arial; font-size: small; "><br></div><div style="font-family: arial; font-size: small; ">2. Why are some constant definitions hidden (e.g. the empty list [] and the list constructor (::)) while others are not (e.g. boolean connectives)?</div><div style="font-family: arial; font-size: small; "><br></div><div style="font-family: arial; font-size: small; ">3. The packaging of real numbers is a bit odd. It is only split in two, very unbalanced packages, real-def and real-thm, and most of the theory is squeezed into the first one, resulting in a huge monolithic package (compare this to the theory of natural numbers). Is this intended or is it still a work in progress?</div><div style="font-family: arial; font-size: small; "><br></div><div style="font-family: arial; font-size: small; ">Regards,</div><div style="font-family: arial; font-size: small; "><br></div><div style="font-family: arial; font-size: small; ">Ali Assaf</div></div></body></html>