Search results

Role for presenting option-setting syntax with proper hyperlinks

Status: Open.

#412 In leanprover/verso;

· david-christiansen opened on May 29, 2025

Inline Lean in manual genre: directives for namespaces and sections

Status: Open.

#411 In leanprover/verso;

· david-christiansen opened on May 29, 2025

Concise role for writing examples of tactics in inline Lean mode in the manual genre

Status: Open.

#410 In leanprover/verso;

· david-christiansen opened on May 29, 2025

Hiding values of <code>let</code> declarations in Verso

Status: Open.

#396 In leanprover/verso;

· 0art0 opened on May 15, 2025

"go to source" code feature in docs?

Status: Open.

#372 In leanprover/verso;

· alok opened on Apr 22, 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