My feeling is that this is not desired.
I’ll make an issue on github for it.
Thanks,
Michael
On 27/6/17, 06:56, "Chun Tian (binghe)" <binghe.l...@gmail.com> wrote:
Hi,
Recently I found that, GENL and Q.GENL has different generalization orders:
> GENL [``x``, ``y``, ``z``] (SPEC_ALL EQ_TRANS);
val it =
|- ∀x y z. (x = y) ∧ (y = z) ⇒ (x = z):
thm
> Q.GENL [`x`, `y`, `z`] (SPEC_ALL EQ_TRANS);
val it =
|- ∀z y x. (x = y) ∧ (y = z) ⇒ (x = z):
thm
see the differences: “!x y z” and “!z y x”. It seems that Q.GENL processes
the variable list in a reverted order.
But SPECL and Q.SPECL has no such differences when specializing a list of
variables:
> SPECL [``a``, ``b``, ``c``] EQ_TRANS;
val it =
|- (a = b) ∧ (b = c) ⇒ (a = c):
thm
> Q.SPECL [`a`, `b`, `c`] EQ_TRANS;
val it =
|- (a = b) ∧ (b = c) ⇒ (a = c):
thm
Q.GENL is not documented currently. But is the behavior desired or not?
Regards,
Chun Tian
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
