Eric Wieser
Eric Wieser
Quoting the docstring: `fast_instance% inst` takes an expression for a typeclass instance `inst`, and unfolds it into constructor applications that leverage existing instances. For instance, when used as ```lean instance...
The relevant test case is ```lean def wrapped_nat (n : nat) := nat structure with_wrapped : Type := (n : nat) (m : wrapped_nat n) #check with_wrapped.mk.inj_eq ``` The diff...
### Prerequisites * [X] Put an X between the brackets on this line if you have done all of the following: * Checked that your issue isn't already [filed](https://github.com/leanprover-community/lean/issues). *...
The contract of `LatexPrinter`'s `_latex` method is to return math-mode latex. However, for `TableForm` it returns in text mode, which leads to invalid latex for code like ```python from sympy...
Some bizarreness means that there are three heads for the original brigl: https://bitbucket.org/msx80/brigl/commits/branch/default I have a "fork" (read: unpacked tarball and `git init`) based off another one of these heads...
Would be good to mention in the readme.
In creating authors for pygae/clifford, we added a `.zenodo.json` like: ```json { "creators": [ { "name": "The Pygae Team" } ], } ``` However, if we leave it at that,...
Without child selectors, the `ul li` styles would be applied to `ul li ol li`, which makes numbering disappear. `li`s should always be selected via a child selector. `ul` and...
Over at pygae/galgebra, a lot of my release notes are of the form `The function :func:`useless_function` was deprecated`. Since these are neither features nor bugfixes, we're currently categorizing them as...
This is now fully covered by https://github.com/leanprover-community/mathlib4/pull/6778