Re: [isabelle] quickchecking lemma with types defined by typedecl
On 19/05/2014 13:28, YuHui Lin wrote:
> 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"
> What do I miss here ? Thanks in advance.
Quickcheck cannot work with types that are merely declared with typedecl.
> 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