[isabelle-dev] Codegen and generic numerals

Makarius makarius at sketis.net
Thu May 17 15:29:04 CEST 2012


Another fine point that showed up in Isabelle2012-RC2 last Monday:

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.


 	Makarius


More information about the isabelle-dev mailing list