Re: [isabelle] Wellsortedness error in code equation Gcd_nat_inst.Lcm_nat



On 11/12/2013 08:29 PM, Florian Haftmann wrote:
Hi Walther,

for the moment it is best to add this declaration to your theory:

lemma [code]:
   fixes ns :: "nat list" and ks :: "int list"
   shows
     "Gcd (set ns) = fold gcd ns 0"
     "Lcm (set ns) = fold lcm ns 1"
     "Gcd (set ks) = fold gcd ks 0"
     "Lcm (set ks) = fold lcm ks 1"
   by (fact Gcd_set_nat Lcm_set_nat Gcd_set_int Lcm_set_int)+

aah, great !
This amend a historic accident that no proper code equations have ever
been declared neither for Gcd nor Lcm.

Again found something for the next release ;-)

So it it's time again to look forward for yet another Isabelle release ;-))
Hope this helps,
	Florian

Thanks a lot,
Walther




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