[opentheory-users] duplicate assumptions for "thm"

[Joe Leslie-Hurd]

Hi Ramana,

Thanks for bringing this up. I would expect most use-cases of the
article format to export theorems with no hypotheses, but it's good to
clarify the desired behaviour on all inputs.

In this case I think there is a missing constraint on the thm command
that the hypothesis list is distinct w.r.t. alpha-equivalence. I've
now made this constraint explicit in the standard:

http://www.gilith.com/research/opentheory/article.html#thmCommand

I've also updated the opentheory tool to detect violations of this
constraint, so from version 1.3 (release 20150102) it will produce
errors of the following form:

$ opentheory info foo.art
FATAL ERROR: opentheory failed:
error in file "foo.art" around line 31:
thm
4
remove
while executing thm command:
alpha-equivalent hypotheses in sequent

Cheers,

Joe

On Thu, Dec 25, 2014 at 5:01 AM, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
> Hi all,
>
> I have a nitpicking question about the "thm" command for OpenTheory
> articles. If the list of terms (t1,...,tn) contains two alpha-equivalent but
> syntactically distinct terms, which one of them should be chosen as the
> representative in the resulting Thm object? Or can we assume that the list
> is all distinct (up to alpha) (in which case, could that be noted
> explicitly)?
>
> Cheers,
> Ramana
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>