Email Gateway (Aug 18 2022 at 14:32): Email Gateway (Aug 18 2022 at 14:32):From: Peter Lammich <peter.lammich@uni-muenster.de>
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
Email Gateway (Aug 18 2022 at 14:32):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Peter,
record ('a,'b) test =
test :: "('b*'a) set"I get the following error:
*** Type unification failed
*** Type error in application: Incompatible operand type
this is definitely not the intended behaviour. Thanks for reporting
this, it will be eradicated in the next release. If this fault does
block your development seriously, we can discuss possible provisional
solutions offline.
Hope this helps,
Florian
*** 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
Last updated: Apr 25 2024 at 12:23 UTC