Re: [isabelle] Wellsortedness error in code equation Gcd_nat_inst.Lcm_nat
for the moment it is best to add this declaration to your theory:
> lemma [code]:
> 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)+
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 ;-)
Hope this helps,
This archive was generated by a fusion of
Pipermail (Mailman edition) and