Re: [isabelle] Problem with quickcheck in Isabelle2015
> I have the following strange behavior of quickcheck on the following
> simple theory:
> datatype t= A | B "(t list)"
> value "B [A,A]"
the "datatype" command has been replaced with a newer implementation since
Isabelle2012. That replacement also meant reimplementation of the old
facilities. Unfortunately, not everything was/could be implemented. I've
stumbled over the same problem before*: Quickcheck generators will only be
installed for datatypes without nested recursion.
Note that the old "datatype" command is still around:
old_datatype t= A | B "(t list)"
fun f:: "t ⇒ bool" where "f _= True"
lemma "f (x::t)= True"
There, the call succeeds. I wouldn't recommend using it, though.
* see also Andreas Lochbihler's mail:
This archive was generated by a fusion of
Pipermail (Mailman edition) and