Search results

Native install instructions don't work

Status: Open.

#115 In leanprover-community/lean4-mode;

· jgarvin opened on Feb 10, 2026

Debugging lean4-mode with lsp

Status: Open.

#114 In leanprover-community/lean4-mode;

· algebravic opened on Dec 23, 2025

Status of this project and relation to <code>nael-mode</code>

Status: Open.

#112 In leanprover-community/lean4-mode;

· dschrempf opened on Oct 15, 2025

<code>indent-region</code> and indentation in general not working properly

Status: Open.

#109 In leanprover-community/lean4-mode;

· clementblaudeau opened on Jul 1, 2025

Unknown request method: workspace/inlayHint/refresh

Status: Open.

#108 In leanprover-community/lean4-mode;

· DarkWingMcQuack opened on Jun 8, 2025

Remove automatic version detection

Status: Open.

#104 In leanprover-community/lean4-mode;

· mekeor opened on Apr 23, 2025

·  

3. Breaking: Refactor

<code>lean4-mode</code> is not automatically activated by <code>.lean</code> files using README instructions

Status: Open.

#103 In leanprover-community/lean4-mode;

· scuellar opened on Apr 10, 2025

Document the pitfall of modifying <code>lean4-mode-hook</code> before Lean4-Mode has been loaded

Status: Open.

#101 In leanprover-community/lean4-mode;

· JLimperg opened on Feb 24, 2025

Certain blackboard font characters break syntax-checking

Status: Open.

#99 In leanprover-community/lean4-mode;

· caelanritter opened on Jan 16, 2025

·  

5. Features and Bugs

Code navigation

Status: Open.

#98 In leanprover-community/lean4-mode;

· ajirving opened on Dec 8, 2024

·  

5. Features and Bugs

Info View without separate window

Status: Open.

#95 In leanprover-community/lean4-mode;

· ultronozm opened on Dec 5, 2024

·  

5. Features and Bugs

Hover docs in info view

Status: Open.

#94 In leanprover-community/lean4-mode;

· ultronozm opened on Dec 5, 2024

·  

5. Features and Bugs