Thank you very much, it works! --Chun
On 23 July 2017 at 02:17, Konrad Slind <konrad.sl...@gmail.com> wrote:
> 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
>>
>>
>
--
Chun Tian (binghe)
University of Bologna (Italy)
------------------------------------------------------------------------------
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
