Re: [isabelle] quickchecking lemma with types defined by typedecl



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.
> 




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