Search results

"go to source" code feature in docs?

Status: Open.

#372 In leanprover/verso;

· alok opened on Apr 22, 2025

md4lean doesn't build on macos: __DATA_CONST segment missing SG_READ_ONLY flag

Status: Open.

#366 In leanprover/verso;

· alok opened on Apr 14, 2025

Manual genre: title overlaps menu button

Status: Open.

#362 In leanprover/verso;

· david-christiansen opened on Apr 11, 2025

bug: use of wrong docstring for tactic

Status: Open.

#351 In leanprover/verso;

· joneugster opened on Apr 4, 2025

Make it possible to hide details of strucures or inductive types in docstring rendering

Status: Open.

#323 In leanprover/verso;

· david-christiansen opened on Mar 13, 2025

Indicate expected import in docstrings

enhancementNew feature or requestNew feature or request

Status: Open.

#320 In leanprover/verso;

· david-christiansen opened on Mar 12, 2025

Don't show ... for proofs in signatures in docstrings

Status: Open.

#319 In leanprover/verso;

· david-christiansen opened on Mar 10, 2025

RFC: Include widget messages in HTML output

Status: Open.

#311 In leanprover/verso;

· Vtec234 opened on Feb 22, 2025

Feature suggestion: <code>{leanWithScope}</code>

Status: Open.

#297 In leanprover/verso;

· nomeata opened on Feb 13, 2025

indented signature leaks indent into the result

Status: Open.

#291 In leanprover/verso;

· nomeata opened on Feb 11, 2025

bug(tactic): Unexpected horizontal rule (thematic break) in parsed Markdown

Status: Open.

#277 In leanprover/verso;

· joneugster opened on Jan 26, 2025

Syntax-highlight comments in verso code

Status: Open.

#274 In leanprover/verso;

· eric-wieser opened on Jan 17, 2025