Re: [isabelle] Isabelle2019-RC2 enat regression



Ah yes, this change set was after the Isabelle2019-RC2 fork point.

Sorry for the noise, then. It’s not a regression, it’s something that hadn’t worked before and now does work in isabelle devel, but not RC2. Nothing that needs to be done.

Cheers,
Gerwin

On 19 May 2019, at 14:50, Denis Nikiforov <denis.nikif at gmail.com<mailto:denis.nikif at gmail.com>> wrote:

Hi

Such expressions began to be simplified after this change:
https://ci.isabelle.systems/jenkins/job/isabelle-all/1171/
So I updated a proof to let the AFP entry build successfully:
https://ci.isabelle.systems/jenkins/job/isabelle-all/1175/
Maybe this change was reverted in the latest revision...


вс, 19 мая 2019 г. в 04:31, Klein, Gerwin (Data61, Kensington NSW) <Gerwin.Klein at data61.csiro.au<mailto:Gerwin.Klein at data61.csiro.au>>:
While updating an AFP entry I found what seems to be a regression for the type enat in Isabelle2019-RC2:

“1 <= (20::enat)” seems to have normalised by simp automatically, but does not any more.

Something like (simp flip: enat_numeral add: one_enat_def) does it, but is not very nice.

Cheers,
Gerwin



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.