Jon Eugster
Jon Eugster
This is a known bug: You must not import a particular level of a different world, only entire worlds. (i.e. `Game.Levels.Tutorial` instead of `Game.Levels.Tutorial.L05add_succ`) leanprover-community/lean4game/issues/60 PS: `add_zero` and `add_succ` are...
I believe this one is by design of the author (aka Kevin Buzzard), similar to how `nth_rewrite` also does not appear in the list but only in the documentation of...
@kbuzzard that's actually a point here. So far we have `nth_rewrite`/`nth_rw` and `repeat rw` as "part" of the `rw` tactic and doc. But `repeat apply` isn't really explained. Should `repeat`...
a) I'm a bit surprised that `FileMap.lines` seems not to be used anywhere else in the code.
@Kha if you want to review/adapt this PR you requested in #3221, please feel free to do so. Otherwise, I'll close it next week as part of cleaning up my...
I have no idea about this. If I rename our `macro` to anything but `rewrite` or `rw`, it shows "unknown identifier 'mul_comm'", but as soon as I name it `rw`...
I think now I'm happy with the functionality and it should be ready for a review.
Might not be a helpful comment, but I'm also just here searching for a way to disable `ctrl + hover` completely.
Here is a working example of how this could be done. Hopefully this could be used to facilitate a proper implementation. The `try`s contain the content of mathlib's `unfold_let` while...
I believe it's only a thing in vscode if you set it in the settings. But I agree, `lean4web` has the option to choose the abbreviation character. Would be nice...