Stream: Beginner Questions

Topic: Automation-friendly distinctness constraint


view this post on Zulip Jakub Kądziołka (Jan 26 2021 at 12:17):

I need to express the assumption that a, b, c and d are pairwise unequal. I'm currently using card {a, b, c, d} = 4, but that's a very automation-hostile form - sledgehammer can barely prove a ~= b. Are there any better options?

view this post on Zulip Mathias Fleury (Jan 26 2021 at 12:19):

distinct [a,b,c,d]?

view this post on Zulip Mathias Fleury (Jan 26 2021 at 12:20):

It compiles down to exactly the disequalities

view this post on Zulip Jakub Kądziołka (Jan 26 2021 at 12:22):

Ah, wonderful!


Last updated: Sep 25 2021 at 09:17 UTC