Hello everyone,
I am trying to prove a theorem using the IEEE floating-point
formalizations of HOL4. In a proof, I need to apply the lemma
lift_ieeeTheory.float_add_relative. However neither match_mp_tac nor
irule are able to unify the lemma with the conclusion I want to show.
I tried instantiating variables by hand to see what happens. Trying the
below code fails with an error complaining about mismatched types in the
conclusion:
SPEC ``(fp64_to_float v):(52, 11) float`` float_add_relative
Can someone tell me what I a doing wrong in this case, since (52,11)
float should be unifiable with (τ, χ) float.
Thanks,
Heiko
------------------------------------------------------------------------------
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
