Re: [isabelle] strange behaviour with type instantiation



Hi Florian,


instantiation  list :: (type) ord
begin

definition le_list_def : "s \<le> t \<longleftrightarrow> (\<exists> r. s @ r = t)" definition less_list_def: "(s :: 'a list) < t \<longleftrightarrow> s \<le> t \<and> s \<noteq> t"

...


did you actually try this ?

I did of course, among other variants, and I still get:

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"
(*
definition less_list_def : "less \<equiv> \<lambda> x y. (x \<le> y \<and> x \<noteq> y)"
*)
instance  ..

end

and still get the same error message:

*** Bad head of lhs: existing constant "op <"
*** The error(s) above occurred in definition: "s < t == s <= t & s ~= t"
*** At command "definition".


Best,

bu







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