Email Gateway (Aug 22 2022 at 19:53): Email Gateway (Aug 22 2022 at 19:53):From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@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
Email Gateway (Aug 22 2022 at 19:53):From: Denis Nikiforov <denis.nikif@gmail.com>
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@data61.csiro.au>:
Email Gateway (Aug 22 2022 at 19:53):From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
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
Last updated: Apr 26 2024 at 08:19 UTC