[add] Update PartialSetoid reasoning #2689
Conversation
| singleStep : ∀ x → x IsRelatedTo x | ||
| multiStep : ∀ {x y} (x∼y : x ∼ y) → x IsRelatedTo y | ||
| reflexive : ∀ {x y} → x ≡ y → x IsRelatedTo y | ||
| relTo : ∀ {x y} (x∼y : x ∼ y) → x IsRelatedTo y |
There was a problem hiding this comment.
Rename constructors to stay closer to Single reasoning
|
Just to check: do these additions/changes fix the issues identified under the original PR? |
|
@jamesmckinna Yes, this will solve the issue by removing any eager pattern matching on propositional equality proofs. I will update this PR's description so that merging this closes the other PR. edit: The description is now updated. |
|
This will also need a |
|
@jamesmckinna Changelog entry is added. |
|
@MatthewDaggitt Fixed! Thanks for the comments. |
|
How to label this one?
|
|
@jamesmckinna It seems like @MatthewDaggitt considers this as a bug fix. I think it is a breaking change, but since no one actually come up with an issue or a PR about the problem in #2677, maybe this one is not so impactful to become a "real" breaking change. |
|
For me, it's more a case of: let's decide, then merge for v2.3, or defer to the next release... |
|
@jamesmckinna I'm not sure it's okay for me to say this, but let's merge this for v2.3 if no one objects. |
There was a problem hiding this comment.
Thanks for the changes @Ailrun. I'm happy to consider this a bugfix as this was the intended behaviour. Let's merge in v2.3.
Resolves #2677.
This one replaces the previous reasoning type for
PartialSetoidwith one properly supporting propositional equality steps.