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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and