Gabriel Ebner
Gabriel Ebner
This resolves the diamond between `Decidable` and `BEq`, which is starting to cause lots of headaches in mathlib.
This adds two features to `#eval` that I've wanted for a long time. - Interactive expressions and traces. - Doesn't refuse to evaluate terms that have missing `Repr`/etc. instances. `#eval...
The parsers for little-endian 16- and 32-bit numbers did not have any specification lemmas at all. The others did not have any constraints on the number of consumed bytes. (Although...
This adds an additional `as_serializer : t:typ ... -> serializer (as_parser t)` function to the 3D interpreter. Some notable complications: 1. In order to have serializers, we need to change...
I am trying to generate a unified dataset of the modules in Everest, where every module name occurs exactly once (i.e., where you can put all the source files in...
The generated files build just fine nowadays.
The `recommend` tactic searches for lemmas in the current environment that look like they could be useful to prove the current goal. It is based on premise selection heuristic used...
This PR adds a package for the Unicode abbreviations used by the [editor](https://github.com/leanprover/vscode-lean4) [plugins](https://github.com/Julian/lean.nvim) for the [Lean theorem prover](https://leanprover.github.io/).
Running the current installer doesn't work for the Flatpak version of Firefox no matter whether you run it inside the sandbox or outside on the host. The `.mozilla` and `.local`...