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.
On Sat, Jul 22, 2017 at 4:23 PM, Chun Tian (binghe) <binghe.l...@gmail.com>
wrote:
> 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
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
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
