Gabriel Ebner

> For example if I have a #print ... command and want to try out various pp options above, I can just unfocus the current pin at the #print and...

> Not sure I'm understanding, there is always a current pin, so adding a pin would result in a second pin in the infoview, which is the clutter I want...

Two examples where the markdown highlighting continues after comment ends: ``` /-! # Headlines -/ ``` ``` /-! indented text -/ ``` Looking through lean files in core and mathlib...

Another common instance of the issue is commented-out code: ``` -- #eval `test ```

I certainly prefer the current behavior. Scrolling to the bottom of the diagnostics is rarely what I want. > It seems more natural perhaps to show the goal instead, which...

Oh sorry, that wasn't really clear to me in the first post. Scrolling to the ⊢ is fine.

What `nvim-cmp` does (cmp-cmdline seems to be only configuration) is hook into `CmdlineChanged` and insert the completion via `nvim_feedkeys`, we could adopt that for the built-in expander as well.

See also M. Hofmann's thesis [2], which attributes a similar extensionality elimination to Gandy [3]. [2] M. Hofmann, Extensional concepts in intensional type theory (1995). [3] R. Gandy. On the...

Further references: Kohlenbach [4, Section 10.4] also describes this translation, and additionally references an exposition by Luckhardt [5, Chapter 2], who in turn additionally cites Takeuti [6] and Schütte [7]...

Jeremy told me in Oxford that such an elimination was already described in the first version of the Principia Mathematica, but I could not find it after a quick look.