[ add ] Data.List.Fresh.Membership.DecSetoid#2914
Conversation
jamesmckinna
left a comment
jamesmckinna
left a comment
There was a problem hiding this comment.
Thanks very much for this.
It all looks good, but I've offered suggestions which might sharpen what you have.
| variable | ||
| r : Level | ||
|
|
||
| _∈?_ : {R : Rel A r} → (x : A) → (xs : List# A R) → Dec (x ∈ xs) | ||
| x ∈? xs = any? (x ≟_) xs |
There was a problem hiding this comment.
The explicit expansion to use Dec might indeed be annoying. I'm not sure it would necessarily be an improvement (readability?), though, to open import Relation.Binary.Definitions using (Decidable), and then have
private
variable
r : Level
R : Rel A r
------------------------------------------------------------------------
-- Re-export contents of propositional membership
open import Data.List.Fresh.Membership.Setoid setoid public
------------------------------------------------------------------------
-- Other operations
infix 4 _∈?_ _∉?_
_∈?_ : Decidable (_∈_ {R = R})
x ∈? xs = any? (x ≟_) xsinstead?
There was a problem hiding this comment.
The explicit expansion to use Dec might indeed be annoying
It's not that annoying imho. In the opening message I was just trying to address question that I thought might pop up.
There was a problem hiding this comment.
But thanks for encouraging the question!
It may be that I am irritated by having to supply so much quantifier prefix/inlined terms in order to get past the typechecker, so I thought it worth exploring the alternatives, notwithstanding @JacquesCarette 's reservations concerning #697 ...
See #2916 for such an exploration, following my suggestions above.
There was a problem hiding this comment.
And thanks for taking my suggestions... I think it does look cleaner now. I think we can merge this now, but suggest waiting till Monday in case any of the other maintainers have strong views on the matter!
There was a problem hiding this comment.
It may be that I am irritated by having to supply so much quantifier prefix/unlined fern in order to get past the typechecker, so I thought it worth exploring the alternative
Sure, although personally I have a knee-jerk reaction whenever I have to apply implicit to operator thinking that I must have done something wrong.
3 participants
I needed to inline
Decidablebecause otherwise Agda wasn't able to figure outr.