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

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)+

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,


PGP available:

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