Hill Bill,
...
0 [`!m. m p == (!q. m * m = 2 * q * q == q = 0)`] (A)
1 [`p * p = 2 * q * q`] (B)
Now a mathematicians would think this means that we have chosen arbitrary
elements of the set that num denotes, and that the variables p and q will
refer to these fixed, but arbitrary,
I bet the information that p, q, and m have type num is stored somewhere.
I know we can infer the type num from the assumptions, but that's not
always true.
Can you tell me where this type information is stored?
Every occurrence of a variable in HOL includes the type of the variable.
You can
