[isabelle] Order of type parameters in record definition



Hi,

Is it intentional that the
order of type parameters of a record must match the occurence of the types in that record?

For example, when trying:
record ('a,'b) test =
 test :: "('b*'a) set"

I get the following error:
*** Type unification failed
*** Type error in application: Incompatible operand type
***
*** Operator:  ??.Code_Evaluation.valapp ::
*** (('b \<times> 'a \<Rightarrow> bool) \<times> 'z \<Rightarrow> ('a, 'b, 'z) test_ext_type) \<times> (unit \<Rightarrow> term) *** \<Rightarrow> (('b \<times> 'a \<Rightarrow> bool) \<times> 'z) \<times> (unit \<Rightarrow> term) *** \<Rightarrow> ('a, 'b, 'z) test_ext_type \<times> (unit \<Rightarrow> term)
*** Operand:   (Abs_test_ext_type, \<lambda>u. <TERM>) ::
*** (('a \<times> 'b \<Rightarrow> bool) \<times> 'z \<Rightarrow> ('b, 'a, 'z) test_ext_type) \<times> (unit \<Rightarrow> term)
***
*** Failed to define record "test"
*** At command "record".

However, defining
record ('b,'a) test =
 test :: "('b*'a) set"

works well.

I could not find this restriction documented in the Reference Manual. Anyway, it's annoying not to be able to specify the type-parameters in the order you want, but in the order Isabelle forces you to do.

Best,
 Peter







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