[ refactor ] Data.List.Relation.Binary.Sublist.Propositional.Properties#2808
[ refactor ] Data.List.Relation.Binary.Sublist.Propositional.Properties#2808jamesmckinna wants to merge 2 commits intoagda:masterfrom
Data.List.Relation.Binary.Sublist.Propositional.Properties#2808Conversation
JacquesCarette
left a comment
JacquesCarette
left a comment
There was a problem hiding this comment.
I think it would make sense to separate the pure additions from the modifications into 2 PRs.
| lookup τ i ≡ lookup τ j → i ≡ j | ||
| lookup-injective {τ = _ ∷ʳ _} = lookup-injective ∘′ there-injective | ||
| lookup-injective {τ = x≡y ∷ _} {here _} {here _} = cong here ∘′ subst-injective x≡y ∘′ here-injective | ||
| lookup-injective {τ = refl ∷ _} {here _} {here _} = cong here ∘′ here-injective |
There was a problem hiding this comment.
This change now makes the comment right after it not make sense?
There was a problem hiding this comment.
Oh, yes. Yuk. Back to the drawing board...
|
|
||
| -- All P is a contravariant functor from _⊆_ to Set. | ||
|
|
||
| All-resp-⊆ : (All P) Respects _⊇_ |
There was a problem hiding this comment.
The name says the opposite of the property?!?!?
There was a problem hiding this comment.
The name is legacy, back-ported from Propositional. But I agree, it's maybe idiotic to have retained it.
There was a problem hiding this comment.
As it's new, there is still time to fix it, right?
There was a problem hiding this comment.
OK, but what about its Propositional specialisation? Add a new name, and deprecate the old one? That might be better, I suppose!?
There was a problem hiding this comment.
Oh... lots of knock-on nonsense. Sigh.
There was a problem hiding this comment.
That would be the logical thing to do (new name, deprecate old).
Ah... yes, you're probably right. But as I comment on the original issue, it's perhaps not even obvious what the right way forward is here. |
2 participants
See #2525 . This tackles the refactoring part, but does not resolve the duplication problem.
UPDATED: yuk... some tricky intensional equality snafus caused by the refactoring. FIXED now, but at the cost of a
breaking(intensional to extensional) change...Not only that, but attempting to deprecate
anti-mono/all-anti-monocauses a dependency cycle betweenData.List.Relation.Unary.All.PropertiesData.List.Relation.Binary.Subset.Propositional.PropertiesI'm tempted to suggest that we make the
breakingchange simply of moving the lemmas to the latter module, and marking this asnon-backwards-compatiblefor the sake of a simpler dependency graph?