Re: [isabelle] value "set [0,0::nat]" = "{0, 0}"::"nat set" – a bug?



Christoph,

Duplication of elements is allowed in sets.

theorem
  "set [0,0::nat] = {0} &
   {0::nat} = {0,0,0,0,0}"
by(simp)

From List.thy:

primrec set :: "'a list => 'a set" where
"set [] = {}" |
"set (x # xs) = insert x (set xs)"

Regards,
GB


On 8/30/2013 10:13 AM, Christoph LANGE wrote:
Dear Isabelle developers,

in Isabelle2013 the expression

value "set [0,0::nat]"

evaluates to

"{0, 0}"
   :: "nat set"

Looks like a bug to me.  Even more so because

value "{0, 0}::(nat set)"

yields

"{0}"
   :: "nat set"

as expected.

Cheers, and have a nice weekend,

Christoph






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.