Re: [isabelle] strange behaviour with type instantiation



Hi Burkhart,
> instantiation  list :: (type) ord
> begin
> 
> definition  le_list_def  : "s \<le> t \<longleftrightarrow> (\<exists>
> r. s @ r = t)"
> 
> definition  less_list_def: "(s::'\<alpha> list) < t
> \<longleftrightarrow> s \<le> t \<and> s \<noteq> t"

This is a misunderstanding how type variables work wrt. instantiation:
type variables for instance specifications are locally fixes during the
whole instantiation block.  Thus you have to write "'a" instead of
"'\<alpha>".

Hope this helps,

	Florian

Attachment: signature.asc
Description: OpenPGP digital signature



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