Cassidy Eastwood (May 01 2026 at 17:45): Cassidy Eastwood (May 01 2026 at 17:45):So, I was trying to use typedef to define a "type of ordered pairs of type 'a × 'a whose first and second place differ (are unequal)". Of course, it's not guaranteed that type will be inhabited for an arbitrary 'a, so I imposed a type restriction using a typeclass for types that have at least two terms. The typedef went through.
However, now any time I use the resulting type, I have to use the type annotation on its type parameter, or I get a type unification error when trying to use any of the actual properties of my type.
My goal in creating this type was to be able to refer to an arbitrary such ordered pair without having to explicitly impose the fst a ≠ snd a condition every time (I'm working on a theory file that frequently deals with such pairs, and types derived from them, and I wanted to clean things up a little). In the end, the need to use this annotation in all the lemmas and constructions for this type is very tolerable, but it strikes me as also a possible indication that I'm doing things in a clumsy way.
My actual question is a bit vague: is this a sensible way of going about this? Is there a better/cleaner approach I should know about?
Kevin Kappelmann (May 01 2026 at 19:01):You could add the constraint in a context:
declare[[show_sorts]]
class non_singleton = assumes non_singleton: "∃x y. x ≠ y"
typedef ('a :: non_singleton) foo = "{p :: 'a × 'a . ∃x y. p = (x, y) ∧ x ≠ y}"
using non_singleton by auto
context fixes dummy :: "'a :: non_singleton"
begin
lemma "P (x :: 'a foo)" (*'a has the right constraint*)
oops
end
I think there's no way to add the sort constraint to the type defined by typedef by default (cf this thread form the mailing list)
Cassidy Eastwood (May 01 2026 at 19:44):I see, thank you!
Last updated: May 05 2026 at 02:56 UTC