[ fix ] Relation.Nullary.Decidable.Core names for combinators
#2843
Conversation
| ... | inj₂ y₁∼x₁ | inj₂ y₂∼x₂ = inj₂ ( y₁∼x₁ , y₂∼x₂) | ||
| ... | inj₂ y₁∼x₁ | inj₁ x₂∼y₂ = inj₁ (sym₁ y₁∼x₁ , x₂∼y₂) | ||
|
|
||
| ×-decidable : Decidable R → Decidable S → Decidable (Pointwise R S) |
There was a problem hiding this comment.
Should this be called pointwise??
There was a problem hiding this comment.
Arguably! But see above below...
|
|
||
| ×-decidable : Decidable _≈₁_ → Decidable _<₁_ → Decidable _<₂_ → | ||
| Decidable _<ₗₑₓ_ | ||
| ×-decidable dec-≈₁ dec-<₁ dec-≤₂ x y = |
| ∷-injective : x ∷ xs ≡ y ∷ ys → x ≡ y × xs ≡ ys | ||
| ∷-injective refl = refl , refl | ||
|
|
||
| ≡-dec : DecidableEquality A → DecidableEquality (Vec A n) |
There was a problem hiding this comment.
Ditto. (this one seems especially egregious, given that conventionally, we make the different choice of _≟_ instead... one reason I wanted to leave this alone, until we could agree a/the 'blessed'/'right' name!) #2845
|
|
||
| module _ {L : REL A B ℓ₁} {R : REL A B ℓ₂} where | ||
|
|
||
| decidable : Decidable L → Decidable R → Decidable (L ∩ R) |
yes, hence the OP reference to "lots of other occurrences of I already encountered the need for some careful qualified importing in order to avoid name clashes, and I didn't want to get into deeper rabbit holes by widening the impact of this PR.
|
2 participants
Fixes #2842
Issues:
-decas a suffix which could/should be changed to?