Hi, every expert.
Maybe I'm a little new to the HOL4 libraries.
But, how could I prove the basic equivalency of rational like `1q / 10
= 10 / 100`?
The documentation is little and I have searched all the source, but
related conversions and tactics like `RAT_EQ_TAC` are all failed and throw
an empty error.
I looked the source about `RAT_EQ_TAC`, which something about
`abs_rat`, and then I become confused.
Sorry for my bothering, and hope the suggestion.
Thanks.
Qiyuan Xu.
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
