lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard
verified publisher icon leanprover

(experimental) fix: match `MonadControlT` to `MonadControl`

Open thorimur opened this issue 2 years ago • 1 comments

Experimental draft PR to utilize CI. Experiments with changing the MonadControlT interface on the basis of this zulip thread to see if it makes sense to open an issue.

thorimur avatar Nov 22 '23 08:11 thorimur

  • ❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-2023-11-22' branch does not exist there yet. We will retry when you push more commits. It may be necessary to rebase onto 'nightly' tomorrow. (2023-11-22 08:56:10)
  • ❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-11-22 22:53:01)
  • ✅ Mathlib branch lean-pr-testing-2944 has successfully built against this PR. (2023-11-23 06:30:19) View Log

leanprover-community-mathlib4-bot avatar Nov 22 '23 08:11 leanprover-community-mathlib4-bot