Kevin Buzzard
Kevin Buzzard
Yeah this PR is something a bit different to `seminorm`, which is for modules. My impression of what's going on here is that both analysts and algebraists want to talk...
I realised that I could implement the entire tactic in "tactic mode". Is that a bit hacky? Issues I failed to deal with: 1) I would like to have better...
@dupuisf and Jireh Loreaux are porting `push_neg` and I think that it would be simpler to wait until that is done before merging this (I'll have to fix the tests...
The `push_neg` PR is #344.
I tried to get this working, now push_neg has been merged, but apparently my code doesn't work any more, I don't know why, and unfortunately I don't have the time...
Oh thanks for the explanation and the fix Gabriel! I'm sorry I didn't finish the job, I don't usually look much at github and I only just now saw the...
Sorry, I only just saw this: I will take a look.
This PR has failed to build because of an unrelated timeout. Junyan has fixed the problem with #16873 so after that has been merged to master someone should merge master...
4. Problem bank directory, with two subdirectories M1F and what_is_mathematics. M1F subdirectory contains numbered lists of problems, with Lean rating. What is mathematics directory contains the basic problems I will...
5. html directory of bits of book which are actually finished? Should do basic title and front page stuff (or at least an html readme generated by sphinx) before I...