> 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 ca
CALL FOR PARTICIPATION
25th International Conference on Computer Aided Verification (CAV 2013)
July 13–19, 2013
Sokos Hotel Palace Bridge, St. Petersburg, Russia
URL: http://cav2013.forsyte.at
HIGHLIGHTS OF CAV
. 53 regular papers, 16 tool papers, 3 invited talks, 4 invited tutorials
. 25th An
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 arbitra
