Search results

Configuration option that limits tactics state popup to checkbox?

Status: Open.

#929 In leanprover/verso;

· IsaacDynamo opened on Jul 17, 2026

First Lean codeblock is corrupted

Status: Open.

#923 In leanprover/verso;

· IsaacDynamo opened on Jul 12, 2026

Squiggly Lean.log lines not shown in lean blocks

Status: Open.

#922 In leanprover/verso;

· whxvd opened on Jul 11, 2026

Controlling multiple simultaneous hover popups

Status: Open.

#921 In leanprover/verso;

· whxvd opened on Jul 11, 2026

Black text on black background on hover with linter.defProp

Status: Open.

#920 In leanprover/verso;

· whxvd opened on Jul 11, 2026

paragraphs are not preserved in docstring boxes in TeX output

Status: Open.

#918 In leanprover/verso;

· medovina opened on Jul 9, 2026

text in references does not appear in TeX output

Status: Open.

#915 In leanprover/verso;

· medovina opened on Jul 9, 2026

"&" in docstring of Html.text is not rendered literally

Status: Open.

#898 In leanprover/verso;

· whxvd opened on Jun 28, 2026

Automatically generated tags for headings are not deduplicated

Status: Open.

#897 In leanprover/verso;

· KBone12 opened on Jun 28, 2026

Links in offline pages

Status: Open.

#865 In leanprover/verso;

· codeguru42 opened on May 31, 2026

Reduce highlighting of search results

Status: Open.

#852 In leanprover/verso;

· Vtec234 opened on May 1, 2026

Lean code fences that use +error in doc.verso docstrings make for broken :literateHtml output

Status: Open.

#842 In leanprover/verso;

· robsimmons opened on Apr 22, 2026