Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] quickchecking lemma with types defined by type...

Email Gateway (Aug 19 2022 at 14:30):

From: YuHui Lin <Y.H.Lin-2@sms.ed.ac.uk>
Hi,

I’ve got an error message when I quickcheck a lemma with types defined by typedecl. A dummy example to illustrate the problem:

typedecl "S"
consts "s" :: "S"
consts "l" :: "S set"

lemma "s : l"
quickcheck

What do I miss here ? Thanks in advance.

regrads,
Yuhui

Email Gateway (Aug 19 2022 at 14:31):

From: Tobias Nipkow <nipkow@in.tum.de>
On 19/05/2014 13:28, YuHui Lin wrote:

Hi,

I’ve got an error message when I quickcheck a lemma with types defined by typedecl. A dummy example to illustrate the problem:

typedecl "S"
consts "s" :: "S"
consts "l" :: "S set"

lemma "s : l"
quickcheck

What do I miss here ? Thanks in advance.

Quickcheck cannot work with types that are merely declared with typedecl.

Tobias

regrads,
Yuhui

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Last updated: Nov 21 2024 at 12:39 UTC