"elim E: x / t" should equate "x" not "t"

The E name is for the closes term on the RHS of colon, not the eliminated one.

@gares I do not understand the statement of the problem. Is it solved?

Still open :-(

It is broken since day one. elim e: a b c/ d. The equation e should talk about a, that is the leftmost term among a b c d.

Today it is always about d.

Shouldn't it be about all the indices?

@gares "day one" is a bit of an overstatement - this did use to work as intended in the original version of the code...

Yea, I mean "day 1 of the implementation of elim I wrote" ;-)

While we are at it:

• in case: I agree that the equation should be abut the leftmost term
• in elim: I've always thought it was a debug feature to see the constructor that generated the current goal; having the equation talk about the eliminated term fits this use case.

@ggonthier do you have a reason for elim (other than consistency)?

I think the debug value is just as good for indexes as it is for main terms, so there's no compelling reason for introducing an inconsistency here. It's not unlikely that the eliminated with dependent indices will not occur at all in the goal, but the indices will, and in that case only the equation on the indices will be useful.