Re: [isabelle] Order of type parameters in record definition



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
> 
> 

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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