[opentheory-users] What's behind the article merging function

[Robert White]

Thanks a lot Joe,

I will merge it up :)

Robert

On 13 July 2015 at 23:06, Joe Leslie-Hurd <joe at gilith.com> wrote:

> Hi Robert,
>
> If you pull the most recent version of the OpenTheory HOL Light fork,
> you can use
>
> list_the_exported_thms ();;
>
> to show a list of exported theorems together with the theory they were
> exported to (i.e., the argument to logfile).
>
> Hopefully that's the information you require.
>
> Cheers,
>
> Joe
>
> On Fri, Jul 10, 2015 at 12:55 AM, Robert White
> <ai.robert.wangshuai at gmail.com> wrote:
> > Dear Joe,
> > Thanks for the reply.
> >
> > Yeah, such a function would be helpful
> >
> > Regards
> > Robert
> >
> > On Jul 9, 2015 8:35 PM, "Joe Leslie-Hurd" <joe at gilith.com> wrote:
> >>
> >> Hi Robert,
> >>
> >> Whenever an article is generated, it is normalized so that if a type
> >> or term is used multiple times then it is built once, saved in a
> >> dictionary, and then pulled out when needed. For theorems this is
> >> taken even further, so that theorems that are alpha-equivalent are
> >> only constructed once.
> >>
> >> I'm afraid there's currently no infrastructure for recording which
> >> article file a theorem was exported to in HOL Light. It probably
> >> wouldn't be too hard to add, though, if you needed the information.
> >>
> >> Cheers,
> >>
> >> Joe
> >>
> >>
> >> On Thu, Jul 9, 2015 at 5:12 AM, Robert White
> >> <ai.robert.wangshuai at gmail.com> wrote:
> >> > Dear Joe,
> >> >
> >> > I wonder what's behind OpenTheory when it's merging two or more
> article
> >> > files together. Is there any optimization?
> >> >
> >> > By the way, for HOL Light, is there any function I can tell which thm
> is
> >> > in
> >> > which article file after exporting?
> >> >
> >> >
> >> > Thanks a lot!
> >> >
> >> > --
> >> >
> >> > Regards,
> >> > Robert White (Shuai Wang)
> >> > INRIA Deducteam
> >> > [Moving to ILLC of UvA from this Sep to continue my masters. ]
> >> > [New email address will be shuai.wang at student.uva.nl]
> >> >
> >> >
> >> > _______________________________________________
> >> > opentheory-users mailing list
> >> > opentheory-users at gilith.com
> >> > http://www.gilith.com/opentheory/mailing-list
> >> >
> >>
> >> _______________________________________________
> >> opentheory-users mailing list
> >> opentheory-users at gilith.com
> >> http://www.gilith.com/opentheory/mailing-list
> >
> >
> > _______________________________________________
> > opentheory-users mailing list
> > opentheory-users at gilith.com
> > http://www.gilith.com/opentheory/mailing-list
> >
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>



-- 

Regards,
Robert White <http://www.dptinfo.ens-cachan.fr/~swang/>(Shuai Wang)
INRIA Deducteam <https://www.rocq.inria.fr/deducteam/>
[Moving to ILLC of UvA from this Sep to continue my masters. ]
[New email address will be shuai.wang at student.uva.nl]
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150713/7df6acf1/attachment.html>