[isabelle] Wellsortedness error in Quickcheck



Hi All:

I met a problem when I try to use test_term in Quickcheck. The lemma is
showed below

*lemma "(f::int => bool) Un (h::int => bool) = h Un f"

*It pops up the following error
***************************************
*** Wellsortedness error:
*** Type int  =>  bool not of sort equal
*** No type arity int :: enum
***************************************

If I change the type from "int => bool"  to "' 'a => bool", then it's fine.
but "nat => bool" is not OK,  "bool => bool" is OK.

Thanks for reading.


Best
Yuhui Lin




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