[opentheory-users] parsing article information

Joe Hurd joe at gilith.com
Mon Jan 10 03:04:45 UTC 2011


Hi Ramana,

> My immediate application would be to check that my reader is correct.
> If I can easily get the set of (term list, term) pairs representing
> theorems that an article is supposed to produce from opentheory, then
> I can check that after reading the article I actually did produce
> those theorems.

Perhaps until there is a better machine-readable format you could use
the "thm" commands in the article that you're reading to simulate
this. If you store the "hyp" and "concl" arguments of each "thm"
command you read, then this is precisely the set of theorems that the
article is supposed to generate.

Cheers,

Joe



More information about the opentheory-users mailing list