Email Gateway (Aug 23 2022 at 08:21): Email Gateway (Aug 23 2022 at 08:21):From: Arvid Marx <arvid.marx@logicandtypes.org>
Hi all,
if I would want to redeclare, say, the notation for partial orders
while still importing Main and Orderings, it seems like I should just
use
no_notation Orderings.ord_class.less_eq (infix "≤" 50)
since there seems to be no other option. However, this apparently
doesn't work, as in
locale preorder =
fixes c :: "'a set"
fixes leq :: "'a ⇒ 'a ⇒ bool" (infix "(≤)" 60)
assumes reflexive : "∀ x ∈ c. x ≤ x"
assumes transitive : "∀x ∈ c. ∀y ∈ c. ∀ z ∈ c. x ≤ y ⟶ y ≤ z ⟶ x ≤ z"
locale partialOrder = preorder +
assumes antisymmetric : "∀ x ∈ c. (∀ y ∈ c. (x ≤ y ⟶ y ≤ x ⟶ x = y))"
reflexive, transitive and antisymmetric still produce heavily ambigous
parse trees that make use of Orderings.ord_class.less_eq, even when
both the constant and the notation is hidden.
I'd appreciate any tips.
Last updated: Nov 21 2024 at 12:39 UTC