Re: [isabelle] Isabelle2019-RC2 enat regression


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

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