2021-11-10: John Major Equality rak
================================================================
John Major equality [0,1] is a form of heterogenous equality
used to simplify statements of equality facts. Adam Chlipala
writes that:
> The identifier JMeq stands for "John Major equality," a name
> coined by Conor McBride as an inside joke about British
> politics. [1]
In McBride's original paper [2], the "inside joke" is:
> I call this 'John Major' equality, because it widens
> aspirations to equality without affecting the practical
> outcome.
I know John Major was prime minister in the 1990s. To what,
exactly, is this joke referring to?
[0]:
https://coq.inria.fr/library/Coq.Logic.JMeq.html
[1]:
http://adam.chlipala.net/cpdt/html/Equality.html
[2]:
http://www.e-pig.org/downloads/elim.pdf
