Hi,
I always understood "fail" as raising "HOL_ERR". However, I might be
wrong there.
There is QCONV. If a conversion raises UNCHANGED, it calls REFL. So
QCONV (REWRITE_CONV thms)
is what you are after, I believe.
Thomas
On 05.05.2017 22:09, Chun Tian (binghe) wrote:
> Hi,
>
> The HOL System REFERENCE said, REWRITE_CONV "Does not fail, but may diverge
> if the sequence of rewrites is non-terminating.”, but I found this is not
> true (any more):
>
>> REWRITE_CONV [ASSUME ``A = B``] ``A``;
> val it =
> [.] |- A = B:
> thm
>> REWRITE_CONV [ASSUME ``A = B``] ``C``;
> Exception- UNCHANGED raised
>
> What I wanted is a theorem ``C = C`` in this case.
>
> Further more,
>
>> REWRITE_CONV [] ``F``
> Exception- UNCHANGED raised
>
> which used to return a theorem ``F = F`` in HOL88:
>
> #REWRITE_CONV [] "F";;
> |- F = F
>
> Is there a way I could get the desired (old) behavior?
>
> 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
> [email protected]
> 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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
