[opentheory-users] Questions about the standard library packages

[Ali Assaf]

Hello, 


I am working on a translation from OpenTheory to Dedukti ( http://www.lix.polytechnique. fr/dedukti/ ), a proof system close to the LF and Coq family. I have some questions regarding the packaging of some theories in the standard library. 


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? 


2. Why are some constant definitions hidden (e.g. the empty list [] and the list constructor (::)) while others are not (e.g. boolean connectives)? 


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? 


Regards, 


Ali Assaf 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20120628/292aa832/attachment.html>