Search results

Add a tool to search in the active page

Status: Open.

#179 In leanprover-community/doc-gen;

· faenuccio opened on Apr 25, 2025

Display of unit.star is glitched

Status: Open.

#175 In leanprover-community/doc-gen;

· Komyyy opened on Nov 27, 2022

Inductive type display is misleading

Status: Open.

#159 In leanprover-community/doc-gen;

· eric-wieser opened on Feb 17, 2022

linkifier misses declarations ending with backticks

Status: Open.

#143 In leanprover-community/doc-gen;

· bryangingechen opened on Nov 12, 2021

named simp sets

Status: Open.

#133 In leanprover-community/doc-gen;

· bryangingechen opened on May 28, 2021

stray backticks at the end of a docstring

Status: Open.

#128 In leanprover-community/doc-gen;

· bryangingechen opened on Mar 30, 2021

sidebar containing declarations (internal_nav) not displayed on mobile

Status: Open.

#119 In leanprover-community/doc-gen;

· bryangingechen opened on Feb 21, 2021

overlapping text on iPad using IOS 12 Safari in landscape mode

Status: Open.

#118 In leanprover-community/doc-gen;

· bryangingechen opened on Feb 21, 2021

"Imported by" misses some files that depend on data.fin.ops

Status: Open.

#108 In leanprover-community/doc-gen;

· bryangingechen opened on Feb 1, 2021

Feature request: add a search page

Status: Open.

#107 In leanprover-community/doc-gen;

· sorawee opened on Jan 17, 2021

Documentation autosearch is not very good

Status: Open.

#104 In leanprover-community/doc-gen;

· BoltonBailey opened on Dec 2, 2020

minisearch webworker is terminated on page reloads

Status: Open.

#96 In leanprover-community/doc-gen;

· eric-wieser opened on Nov 16, 2020