[isabelle-dev] Codegen and generic numerals

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Fri May 18 11:29:41 CEST 2012

> 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.


-------------- 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>

More information about the isabelle-dev mailing list