Brendan Seamas Murphy
Brendan Seamas Murphy
Is there a reason there's no `BindCombinator`? I tried to add one but `Parser.remainder` is internal. Also, is there a reason `Parser.remainder` is internal? I'd prefer the ability to add...
# Summary Changes the types of `MonadControl.restoreM` and `MonadControlT.restoreM`. See https://github.com/leanprover/lean4/issues/2894 for more information, I'm not sure whether the difference between the existing types is or is not intentional
The git history should be a lot nicer now.
Right now, doing IO in the Hackett repl is kind of gross; your only option afaik is to wrap your `IO ()`s in an `unsafe-run-io!` call. Having e.g. `#:run` and...
Informally we show `(R⧸I) ⊗ M = M/IM`. --- - [ ] depends on: #13119 If someone can golf away this dependency I'd be happy! The existing proof that `Submodule.map...
Transport of exact sequences & the behavior under quotienting. --- Noting that this has merge conflicts with PR #13098. I guess whichever is merged second will have to deal with...
Add the definition of regular sequences and induction principles for them. --- Despite the branch name this PR does not define depth. I would appreciate any suggestions on how to...
Add some lemmas about `IsSMulRegular`. --- I'm not sure if it's okay to add the `Mathlib.GroupTheory.GroupAction.Hom` import. My understanding is that this file is kept low in the hierarchy for...
Golf & generalize `smul_top_eq_map`. --- [](https://gitpod.io/from-referrer/)