*To*: Lars Hupel <hupel at in.tum.de>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] inductive + for*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Fri, 15 Apr 2016 17:51:08 +0200*In-reply-to*: <5710FA6B.40608@in.tum.de>*References*: <5710FA6B.40608@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.6.0

Hi Lars,

inductive test' :: "'a â nat â bool" and test :: "nat â 'a â bool" for b where "test a b â test' b a" | "test 0 b" | "test n b â test (Suc n) b" thm test'.induct Hope this helps, Andreas On 15/04/16 16:27, Lars Hupel wrote:

Dear list, it appears that in a "for" clause for inductive definitions, I can only list the parameters in their respective order. That is, I can't state that the second parameter of a definition remains unchanged. Is this intentional? It means that now I have to either reshuffle all uses of my definition or prove a custom induction rule. Cheers Lars

**References**:**[isabelle] inductive + for***From:*Lars Hupel

- Previous by Date: [isabelle] inductive + for
- Next by Date: [isabelle] ZF theory - loading problem
- Previous by Thread: [isabelle] inductive + for
- Next by Thread: [isabelle] ZF theory - loading problem
- Cl-isabelle-users April 2016 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