Skip to content
Add "ready-to-merge" and "delegated" label from comment

[Merged by Bors] - feat(Logic/Basic): add simp lemma for @Exists.choose _ (· = a) _ #47271

Sign in to view logs

[Merged by Bors] - feat(Logic/Basic): add simp lemma for @Exists.choose _ (· = a) _

[Merged by Bors] - feat(Logic/Basic): add simp lemma for @Exists.choose _ (· = a) _ #47271

Triggered via issue July 9, 2024 23:16
@leanprover-botleanprover-bot
commented on #14419 5e75b54
Status Skipped
Total duration 3s
Artifacts –

add_label_from_comment.yml

on: issue_comment
Add ready-to-merge label
0s
Add ready-to-merge label
Add delegated label
0s
Add delegated label
Fit to window
Zoom out
Zoom in