> 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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
