-
Notifications
You must be signed in to change notification settings - Fork 298
[Merged by Bors] - feat(data/option/*): pmap and pbind defs and lemmas #5442
Conversation
pechersky
commented
Dec 20, 2020
src/data/option/defs.lean
Outdated
/-- Partial bind. If for some `x : option α`, `f : Π (a : α), a ∈ x → option β` is a | ||
partial function defined on `a : α` satisfying `p` giving an `option β`, | ||
then `pbind x f h` is essentially the same as `bind x f` | ||
but is defined only when all `x = some a` and the `a` satisfy `p`, using the proof | ||
to apply `f`. -/ | ||
@[simp] def pbind : Π (x : option α), (Π (a : α), a ∈ x → option β) → option β | ||
| none _ := none | ||
| (some a) f := f a rfl |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't see p
anywhere in the code - is this comment wrong? Or should a ∈ x
be p x
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I tried to reword the docstring.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Some initial comments.
src/data/option/basic.lean
Outdated
simpa only [H] using hz } } | ||
end | ||
|
||
@[simp] lemma pbind_eq_bind {f : α → option β} : |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@[simp] lemma pbind_eq_bind {f : α → option β} : | |
@[simp] lemma pbind_eq_bind (f : α → option β) : |
f
is not inferable from later arguments, is there a reason for it to be implicit here?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe I'm missing something, but isn't it true that we can make arguments implicit if they appear on both sides of an equality or iff, since we usually just use these lemmas in rewriting?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah, sorry, I lost track of this in the craziness of the last few weeks. Yes, for using these in rw
/simp
it doesn't matter, but it does if you want to use them in e.g. have
. For iff
, the lemma_name.mp
only works if all the arguments are implicit, which is a good reason to prefer that. But eq.mp
is less commonly used. That said it's not so important.
I've tried to make arguments more explicit in lemmas, and restructured the lemmas to group eq and iff separately. |
@robertylewis any final comments? |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
bors d+
✌️ pechersky can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
bors r+ |
Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |