*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Wellsortedness error in code equation Gcd_nat_inst.Lcm_nat*From*: Walther Neuper <wneuper at ist.tugraz.at>*Date*: Tue, 12 Nov 2013 17:18:32 +0100*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.1.0

When generalizing the following function from definition primitive :: "int poly ⇒ int × int poly" to definition primitive :: "'a::{ring_div,Gcd} poly ⇒ 'a × 'a poly" where "primitive p = ( let d = Gcd (set (coeffs p)) in (d, (*sdiv d*) p))" this is accepted by the system (with "sdiv d" as well).

value "primitive [:2::int, 4, 6, 8:] = (2, [:1, 2, 3, 4:])" Wellsortedness error (in code equation Gcd_nat_inst.Lcm_nat ?m ≡ if finite ?m then Finite_Set.fold gcd_nat_inst.lcm_nat one_nat_inst.one_nat ?m else zero_nat_inst.zero_nat): Type nat not of sort finite No type arity nat :: finite

If not, any hint is appreciated! Many thanks in advance, Walther

**Attachment:
Two_Sorts.thy**

**Follow-Ups**:**Re: [isabelle] Wellsortedness error in code equation Gcd_nat_inst.Lcm_nat***From:*Florian Haftmann

- Previous by Date: [isabelle] find sessions
- Next by Date: Re: [isabelle] Remaining reasons for Proof General
- Previous by Thread: Re: [isabelle] find sessions
- Next by Thread: Re: [isabelle] Wellsortedness error in code equation Gcd_nat_inst.Lcm_nat
- Cl-isabelle-users November 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list