Skip to content
Open
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions src/libexpr/primops.cc
Original file line number Diff line number Diff line change
Expand Up @@ -4014,6 +4014,8 @@ static RegisterPrimOp primop_sort({

1. Transitivity

If a is less than b; b is less than c. Then it follows that a is less than c
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
If a is less than b; b is less than c. Then it follows that a is less than c
If a is less than b and b is less than c, then it follows that a is less than c.


```nix
comparator a b && comparator b c -> comparator a c
```
Expand All @@ -4026,6 +4028,9 @@ static RegisterPrimOp primop_sort({

1. Transitivity of equivalence

If a is NOT less than b; b is NOT less then a; a and b are equal according to the comparator.
If b is equal to c then it follows that a is equal to c
Comment on lines +4031 to +4032
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
If a is NOT less than b; b is NOT less then a; a and b are equal according to the comparator.
If b is equal to c then it follows that a is equal to c
First, let us define *equivalence* with respect to some comparator:
If x is *not* less than y and x is *not* less then y, then x and x are equivalent according to the comparator.
Having done that, now we can define the transitivity of this equivalence:
If a is equivalent to b and b is equivalent to c, then it follows that a is equivalent to c,

I think using different variables here make the prose much less confusing. Your version IMO made the mistake of extending the a: b: ... scope too far: the second a and b are not the same.

Copy link
Contributor Author

@hsjobeki hsjobeki Nov 13, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Okay, i can make the sentence more correct in that regard. But my other point was to avoid the term transitivity in its own definition. Because at that point i (or the reader) doesn't understand what it means.

I also wonder if we need to define the eq function, when the point is to explain the concept, we shouldn't over formalize, but make sure the required property is understood by keeping the explanation simple.


```nix
let equiv = a: b: (!comparator a b && !comparator b a); in
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
let equiv = a: b: (!comparator a b && !comparator b a); in
let equiv = x: y: (!comparator x y && !comparator x y); in

equiv a b && equiv b c -> equiv a c
Expand Down
Loading