Bryan Gin-ge Chen
Bryan Gin-ge Chen
Reported by @kodyvajjha on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Lean.20crashing/near/167582186). The following code crashes both 3.4.2 and the latest 3.5.0c nightly ("nightly-2019-05-17"): ```lean universe u open nat variable {α : Type u} def vec :...
I wish we could see how the tactic state changes before and after semicolons. I asked Mario about this in this Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/semicolon.20and.20tactic.20state Apparently this requires changes to the...
Here's a list of "primed" tactics in mathlib which fix bugs or add features to tactics in the core library. I'm not sure which of these should replace their counterparts,...
I noticed that the build in #23 was failing due to some outdated actions. Hopefully this will fix the build!
Hi, thanks for this very convenient action! We've been using it for a while at https://github.com/leanprover-community/mathlib (see [here](https://github.com/leanprover-community/mathlib/blob/master/.github/workflows/merge_conflicts.yml)), but recently the action has been failing on every run with the...
As requested on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/paste.20the.20goal.20at.20the.20cursor)
Is there a way to have the extension run `leanproject get-mathlib-cache` or `leanproject get-cache` if we "obviously" need to? [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Memory.20consumption.20of.20mathlib/near/214258914)
Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Sever.20sharing.20in.20live.20share/near/202056350 I can try to take a crack at this after the widget refactor settles.
The [linter](https://github.com/leanprover-community/mathlib/blob/master/docs/commands.md#lint) provided by mathlib is now fairly sophisticated. We should see if we can better integrate it with the extension. One idea is to make `#lint` output something which...
When a user hovers over notation in the infoview we should be able to pop up a tooltip with the info about how to type that character. See [Zulip discussion](https://leanprover-community.github.io/archive/113488general/03279VScodegoodies.html#181283954)....