Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Wellsortedness error in Quickcheck

Email Gateway (Aug 18 2022 at 18:22):

From: Yuhui Lin <lyhlbsl@gmail.com>
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

Last updated: Apr 20 2024 at 04:19 UTC