Gabriel Ebner
Gabriel Ebner
Since a few weeks ago, the proof for the `char.zero_lt_d800` theorem in the core library has almost a trillion subterms if we count them as a tree: ```lean open expr...
There is at least one snippets that does not work with the current lean 2 version, in `10_Structures_and_Records.org`: ```lean import standard open nat structure big := (field1 : nat) (field2...
The attribute elaborator checks whether `move` is a string literal, which it is not.
When posting issues to Zulip you often want to copy the whole trace, right now the only way to get that is to either 1) manually expand all the subtraces,...
```lean def N : Nat := Nat.add 37 50 example : N ≠ N := by simp (config := {decide := false}) only [N, Nat.add] /- Put cursor on `≠`...
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/VSCode.20toc/near/200764479
Maybe all warnings?
Multi-root workspaces have not landed in stable vscode yet as of the June 2017 release, but I expect them to be released soon and we'd better be ready for them....
We try to add `c:/msys64/mingw64/bin` to the path on windows, since that's where the shared libraries are for msys2, and otherwise lean won't find them. This doesn't seem to work...