[isabelle] quickchecking lemma with types defined by typedecl
I’ve got an error message when I quickcheck a lemma with types defined by typedecl. A dummy example to illustrate the problem:
consts "s" :: "S"
consts "l" :: "S set"
lemma "s : l"
What do I miss here ? Thanks in advance.
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
This archive was generated by a fusion of
Pipermail (Mailman edition) and