fix: elaborate the do continuation only once when contracting pure () - #15682

fix: elaborate the do continuation only once when contracting pure ()#15682

sgraf812 merged 2 commits into

masterleanprover/lean4:masterfrom

sg/issue-13858leanprover/lean4:sg/issue-13858Copy head branch name to clipboard