Julian/lean.nvim

Issues

• is there a way to toggle showing results of '#eval' and '#check'

  #360 opened 3 months ago by CadeMichael
  1

• Feature request: Jump to corresponding file and line in trouble.nvim diagnostics

  #359 opened 3 months ago by utensil
  1

• Infoview error fires whenever the current buffer changes

  #351 opened 3 months ago by ray-kast
  9

• Provide option to unbind default <Tab> and <CR> bindings for abbreviation expansion

  #355 opened 3 months ago by ElectronSutra
  1

• Setting `ft` configuration causes an error on startup

  #353 opened 4 months ago by Ben10164
  7

• "CalcPanel" is not a supported Lean widget type.

  #352 opened 5 months ago by jcommelin
  1

• Show a sign column indicator for how far the cursor is from where is being processed

  #349 opened 5 months ago by Julian
  1

• Recommend a minimap plugin with configurable processing information

  #350 opened 5 months ago by Julian
  0

• Action to accept lean's suggestion

  #347 opened 6 months ago by yakimk
  2

• Closing the infoview buffer with :q! causes errors

  #346 opened 6 months ago by stephen-huan
  3

• lean.nvim emits logs on other files to ~/.local/state/nvim.log

  #343 opened 6 months ago by MangoIV
  2

• Visual Indicator for Infoview pause

  #344 opened 6 months ago by JadAbouHawili
  1

• Deprecated Commands in Neovim 0.11

  #342 opened 6 months ago by ArvinSKushwaha
  1

• Inaccessible hypothesis highlighting should highlight inaccessible names even when there are alternate accessible ones

  #326 opened 6 months ago by Julian
  0

• Entering edit mode will shrink line-number bar, moving text around

  #340 opened 7 months ago by VictorTaelin
  3

• How can i help the project?

  #341 opened 7 months ago by RamonJales
  5

• Set winfixbuf when available (0.10+) on our infoview windows.

  #332 opened 8 months ago by Julian
  0

• Files opened under */src/lean/ are unmodifiable

  #333 opened 10 months ago by mars0i
  9

• Infoview tooltips should render their contents as markdown

  #329 opened a year ago by Julian
  1

• neovim can freeze up / use 100% CPU when editing or navigating around Lean files

  #289 opened a year ago by Karthik-Dulam
  5

• Spawning language server with cmd: `lean` failed

  #330 opened a year ago by aagontuk
  1

• (Re-)review / harmonize with the VSCode options

  #328 opened a year ago by Julian
  0

• Musl usage error message

  #324 opened a year ago by foxyseta
  4

• Infoview autoclose

  #323 opened a year ago by frangio
  1

• highlights.scm: @boolean -> @constant.builtin.boolean, @repeat -> @keyword.control.repeat

  #319 opened a year ago by josephholsten
  4

• Improve `:Telescope loogle`

  #317 opened a year ago by hargoniX
  1

• Help for a newbie

  #320 opened a year ago by ykonstant1
  3

• Client 1 quit with exit code 0 and signal 11

  #322 opened a year ago by arbitrary-dev
  5

• Anonymous sections aren't treated as a pair

  #310 opened a year ago by stephen-huan
  1

• "Try this" replaces incorrect segment

  #313 opened a year ago by grhkm21
  6

• Consider making the max width / height of infoviews work via percentages of real estate rather than columns/rows

  #315 opened a year ago by Julian
  0

• git password prompt in lakefile breaks neovim

  #274 opened 2 years ago by gebner
  3

• Unicode LaTeX tab completion

  #309 opened a year ago by chakravala
  10

• nvim-treesitter: upstream Tree-Sitter grammar and queries

  #304 opened a year ago by XVilka
  6

• Find executable via `elan which`

  #305 opened a year ago by RaitoBezarius
  7

• checkhealth error: failed to run healthcheck for "lean" plugin

  #300 opened a year ago by dsb-y
  1

• Correct way to quit neovim while the plugin is running

  #290 opened a year ago by tomaz1502
  2

• Distinguish \perp and \bot

  #296 opened 2 years ago by MithicSpirit
  1

• Highlight inaccessible hypotheses differently in Lean 4

  #271 opened 2 years ago by Julian
  0

• Cursor jumps around when infoview is open

  #286 opened 2 years ago by prescientmoon
  8

• Error executing `vim.schedule` via lua callback

  #284 opened 2 years ago by mdgeorge4153
  4

• Error while calling lua chunk: ~/.config/nvim/plugin/lean.lua:10: module 'cmp' not found

  #285 opened 2 years ago by mdgeorge4153
  2

• Error executing vim.schedule lua callback

  #283 opened 2 years ago by mattrobball
  2

• Error for files with special characters in path name

  #282 opened 2 years ago by ianjauslin-rutgers
  3

• Have to set ft=lean3 to hook lean3ls

  #281 opened 2 years ago by fecet
  4

• Syntax highlighting within {} blocks

  #278 opened 2 years ago by carl-westerlund
  1

• attempt to index global 'lean_nvim_ft_options' (a nil value)

  #275 opened 2 years ago by OmeletWithoutEgg
  3

• ftdetect script references rest of plugin

  #272 opened 2 years ago by 4e554c4c
  2

• Abbreviation mappings are broken in the presence of user mappings which are lua callbacks

  #270 opened 2 years ago by Julian
  0

• Specify location of lsp

  #266 opened 2 years ago by DieracDelta
  2