[opentheory-users] definition of "new" constants? / processing of packages

[Ramana Kumar]

Dear Günter,

I can answer some but not all of your questions, and do so below.

On 14 August 2015 at 00:15, Günter Rote <rote at inf.fu-berlin.de> wrote:

> When opentheory processes a theory, does it read all theory article files
> on which it depends?
>

opentheory would need to know the logical content (the theory inputs and
outputs) of the dependencies, in order to calculate the theory inputs and
outputs of the theory being processed. Whether it figures these out by
processing the dependencies or using some caches, I'm not sure.


> Or is there a way that it just needs to read the theorems from
> other packages that it uses?
>

I suspect there is a cache, but Joe would know.


> I can somehow guess what the entry
>   show: "Data.Bool"
> in the .thm file means, but it is not completely clear.
> In particular, what happens when there are several "show: " lines?
>

Each "show: " line adds another bit of namespace that won't need to be
printed. I agree that their exact format and effect is a bit mysterious,
though.


> Is there a way to eventually look at the theorems that are proved
> in detail in an unambiguous format with all type information? (other than
> the html
> format with mouse-over?)
>

I would say that the article itself is this "unambiguous format". If you
want to see a term in any other format, you can write an article parser
that will build the term and then print it however you like.


>
> Best regards :
> --
> G"unter Rote               (Germany=49)30-838-75150 (office)
> Freie Universit"at Berlin                    -75103 (secretary)
> Institut f"ur Informatik       FAX (49)30-838-75192
> Takustrase 9, D-14195 Berlin, GERMANY
>
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150814/fcc808eb/attachment.html>