subject:"\[Hol\-info\] REWRITE_CONV fails"

Re: [Hol-info] REWRITE_CONV fails

2017-05-05 Thread Chun Tian (binghe)

Hi Thomas, Perfect! Thanks very much! This is exactly what I needed. Regards, Chun > Il giorno 05 mag 2017, alle ore 22:15, Thomas Tuerk > ha scritto: > > Hi, > > I always understood "fail" as raising "HOL_ERR". However, I might be wrong > there. > > There is

Re: [Hol-info] REWRITE_CONV fails

2017-05-05 Thread Thomas Tuerk

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

[Hol-info] REWRITE_CONV fails

2017-05-05 Thread binghe

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``;