[isabelle-dev] Codegen and generic numerals

[Florian Haftmann]

> lemma "1 + 1 = 2" by simp  -- works
> 
> value "1 + 1"  -- "(1∷'a) + (1∷'a)"
> value "[1] = [2]"  -- "equal_class.equal (1∷'a) ((1∷'a) + (1∷'a))"
> 
> This is all correct, but maybe a bit unexpected for users.

First, note that all these evaluations stem from nbe rathern than SML
(try value [code] …).  SML fails since it needs to work on concrete types.

Further, the whole code generator infrastructure only allows equations
for overloaded constants at a particular instance, not polymorphic
equations.  Hence a generic rule like »1 + 1 = 2« can not be added.
If you restrict your examples to a particular type (e.g. rat), you get
more reasonable normal forms immediately.

Note that this behaviour has nothing to do with the change in the
numeral representation.

	Florian

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120518/c99f1bb9/attachment.sig>