[isabelle] Problem with quickcheck in Isabelle2015





Dear all Isabelle users,


I have the following strange behavior of quickcheck on the following simple theory:


-------------------------------
datatype t= A | B "(t list)"

value "B [A,A]"

fun f:: "t â bool"
where
"f _= True"

lemma "f (x::t)= True"
quickcheck
quickcheck [tester=narrowing]
-------------------------------

All the quickcheck calls fail. The last one fails with the following error message:

Type unification failed: No type arity t :: narrowing

Type error in application: incompatible operand type

Operator:  ??.Quickcheck_Narrowing.ensure_testable :: ??'a â ??'a
Operand:   Îx. equal_bool_inst.equal_bool (f x) True :: t â bool


Note that the same example works fine with Isabelle2012.


Thanks in advance for any hint,

Best regards,

Thomas
--
Thomas Genet
ISTIC/IRISA
Campus de Beaulieu, 35042 Rennes cedex, France
TÃl: +33 (0) 2 99 84 73 44 E-mail: genet at irisa.fr
http://www.irisa.fr/celtique/genet




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