Julien Narboux
Julien Narboux
The separation between hypothesis and what needs to be proved: ⊢ could be replaced. XYZ: Type AA': Set X f: X → Y g: Y → Z BB': Set Y...
It would be nice to make a release, so that when using Lean Verbose for teaching we can rely on a stable version and won't not risk an involuntary update....
Hi, Thanks a lot for your tool which is excellent. I wanted to add an exercise about how to undo a faulty merge, following: https://www.kernel.org/pub/software/scm/git/docs/howto/revert-a-faulty-merge.txt It seems that when trying...