Gabriel Ebner

Just putting this up as a PR here because CI is disabled on branches.

Required mathlib changes are manageable, as expected: https://github.com/leanprover/std4/compare/pr2060?expand=1 https://github.com/leanprover-community/mathlib4/compare/pr2060?expand=1

!bench

> should the goal-selecting version of show be spelled show e => tac instead? 👍

The code is based on my leanhammer prototype from 2019. I tried it out on some random parts of mathlib. The results are very uneven. Sometimes it finds just the...

This seems to be fixed with the new syntax file. 8190db010334fbdf287a3aa219007cd33780681f

Hi Jason! This plugin is no longer maintained. If you are by any chance using neovim, then please check out our new [lean.nvim](https://github.com/Julian/lean.nvim/) plugin, which has server support to show...

> What would it take to adapt this repo into an ace plugin which [..] can point to an instance of C++ lean running on a server? 1. Write a...

The font size (and family) is taken from the editor font by default. It will also change font size along with the rest of the UI when you press `ctrl++`...

> Yes I found lean4.infoViewStyle, but how do you use it exactly? You can set it to `body { font-size: 30px; }` for example. > I was surprised that this...