[isabelle] locale import
I seem to be unable to extract the necessary information from the locale
documentation. Could somebody explain what happens in the following
locale poset = ord +
fixes A :: "'a set"
assumes lt_le_not_le: "[|x : A; y : A|] ==> x < y <-> x <= y & ~ (y
and refl: "x : A ==> x <= x"
and trans: "[|x : A; y : A; z : A; x <= y; y <= z|] ==> x <= z"
My goal was to reuse the syntax of ord and define a locale capturing
partially ordered sets. However, the above declaration gives me:
fixes less_eq :: "'a ⇒ 'a ⇒ bool"
and less :: "'a ⇒ 'a ⇒ bool"
and A :: "'b ⇒ bool"
assumes "poset A"
And I doen't see why the carrier A does not have elements of the same
type as less_eq and less? How could I achieve this effect?
This archive was generated by a fusion of
Pipermail (Mailman edition) and