Skip to content

fix: mkBindUnlessPure should call the continuation only once#13985

Open
Rob23oba wants to merge 1 commit into
leanprover:masterfrom
Rob23oba:do-pure-cont-fix
Open

fix: mkBindUnlessPure should call the continuation only once#13985
Rob23oba wants to merge 1 commit into
leanprover:masterfrom
Rob23oba:do-pure-cont-fix

fix mkBindUnlessPure calling continuation twice

4b1667a
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
check-pr-body
succeeded Jun 9, 2026 in 5s