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.
On 19 May 2019, at 14:50, Denis Nikiforov <denis.nikif at gmail.com<mailto:denis.nikif at gmail.com>> wrote:
Such expressions began to be simplified after this change:
So I updated a proof to let the AFP entry build successfully:
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and