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 (Num.inc n)"
>   unfolding One_nat_def numeral_inc by simp_all
> 
> declare Num.inc.simps [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.

Cheers,
	Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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