Re: [isabelle] Isabelle2019-RC2 enat regression



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>:

> 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.