[isabelle] making local definitions programmatically
I have a locale L with some number of fixes, f1, f2 and f3, say.
Using LocalTheory.define, I have defined a number of constants in that
locale with eqns
C1 == rhs1
C2 == rhs2
some, none or all of the rhs-es may refer to the fixes. Say each of
C1 and C2 is of type nat.
Subsequently, in the same locale, I want to define a function of the
select b == if b then C1 else C2
I want to build the right-hand side for this definition in ML.
What do I put into the conditional term in the place of C1 and C2?
It would be nice if I could just write
But I guess this won't work, because C1 probably really has a type
that depends on the fixes that appear in rhs1, and likewise C2.
I.e., at the top level, if I do the Isar command
I may see that it really has type "fixtype1 => nat", and L.C2 may have
type "fixtype1 => fixtype2 => nat".
So, what do I do?
This archive was generated by a fusion of
Pipermail (Mailman edition) and