Re: [isabelle] Numeral is acting strangely




Steven Obua wrote:
"2::'a" is just a pretty-printed version of a more complex term. You cannot pretty-print "Numeral0" in that way, because then "Numeral0" would have to become "0", but as you already figured out, "Numeral0" is not the same as "0", therefore this pretty-printing would be maybe intuitive, but wrong.

Thank you, I get it now. It's so easy to get confused when thinking of numbers as numbers! This also means that despite appearing strange, my patch is actually functioning correctly.

Rafal Kolanski.






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