Re: [isabelle] Printing natural numbers

What are the failing examples?  The following works:

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

Odd. I could have sworn this did not work when I tested. But it works now, so even better.

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.

Good. Then I suppose I'll add something like this soon. I am also planning to add some code_post rules to print multisets as "{#1,2,3#}" instead of "mset [1,2,3]".

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