[Hol-info] How to write a general EQ_CONV ?

[Chun Tian (binghe)]

Hi,

If I have two terms s1 and s2 of type ``:string``, then

string_EQ_CONV ``^s1 = ^s2``

returns a theorem like: |- ``^s1 = ^s2 = T`` or |- ``^s1 = ^s2 = F`` about the equality the two terms. But if I don’t know the types of s1 and s2, how can I achieve the same goal by finding a function like string_EQ_CONV and call it?

Regards,

Chun Tian

[Konrad Slind]

EVAL_CONV should do it. It is a general-purpose evaluator that works by
deduction. It may even be that string_EQ_CONV is implemented in terms
of it. The documentation about computeLib in
the Description should tell you more.

Konrad.

Post by Chun Tian (binghe)
Hi,
If I have two terms s1 and s2 of type ``:string``, then
string_EQ_CONV ``^s1 = ^s2``
returns a theorem like: |- ``^s1 = ^s2 = T`` or |- ``^s1 = ^s2 = F``
about the equality the two terms. But if I don’t know the types of s1 and
s2, how can I achieve the same goal by finding a function like
string_EQ_CONV and call it?
Regards,
Chun Tian
------------------------------------------------------------
------------------
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
https://lists.sourceforge.net/lists/listinfo/hol-info

[Chun Tian (binghe)]

Thank you very much, it works! --Chun

Post by Konrad Slind
EVAL_CONV should do it. It is a general-purpose evaluator that works by
deduction. It may even be that string_EQ_CONV is implemented in terms
of it. The documentation about computeLib in
the Description should tell you more.
Konrad.

Post by Chun Tian (binghe)
Hi,
If I have two terms s1 and s2 of type ``:string``, then
string_EQ_CONV ``^s1 = ^s2``
returns a theorem like: |- ``^s1 = ^s2 = T`` or |- ``^s1 = ^s2 = F``
about the equality the two terms. But if I don’t know the types of s1 and
s2, how can I achieve the same goal by finding a function like
string_EQ_CONV and call it?
Regards,
Chun Tian
------------------------------------------------------------
------------------
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
https://lists.sourceforge.net/lists/listinfo/hol-info