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



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

-- 
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701

→ Mathematics in Computer Science Special Issue on “Enabling Domain
  Experts to use Formalised Reasoning”; submission until 31 October.
  http://cs.bham.ac.uk/research/projects/formare/pubs/mcs-doform/




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