Re: [isabelle] Printing natural numbers

Hi Manuel.

> I just realised that the
> following [code_post] rules allow nice printing of natural numbers
> (although computation is still done Peano-style behind the curtain):
> lemma eval_Suc_nat [code_post]:
>   "Suc 0 = 1"
>   "Suc 1 = 2"
>   "Suc (numeral n) = numeral ( n)"
>   unfolding One_nat_def numeral_inc by simp_all
> declare [code_post]
> However, for some reason, this does not seem to work for the [simp] and
> [nbe] evaluators.

What are the failing examples?  The following works:

	value [code] "Suc 42"
	value [nbe] "Suc 42"
	value [simp] "Suc 42"

> Does anyone apart from me think that something like this should be done?

I think the only reason why nobody has ever attempted this so far is
that the old signed numerals did not allow such a simple post processing.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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