Re: [isabelle] Wellsortedness error in code equation Gcd_nat_inst.Lcm_nat
On 11/12/2013 08:29 PM, Florian Haftmann wrote:
for the moment it is best to add this declaration to your theory:
fixes ns :: "nat list" and ks :: "int list"
"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,
Thanks a lot,
This archive was generated by a fusion of
Pipermail (Mailman edition) and