Re: [isabelle] inductive + for
This is indeed a limitation of inductive. The canonical way around it is to define the
constant with the order of arguments as required by inductive and simultaneously an
abbreviation which does the reshuffling. This looks as follows:
inductive test' :: "'a â nat â bool"
and test :: "nat â 'a â bool"
"test a b â test' b a"
| "test 0 b"
| "test n b â test (Suc n) b"
Hope this helps,
On 15/04/16 16:27, Lars Hupel wrote:
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and