search

leanprover / doc-gen4

Document Generator for Lean 4
Apache License 2.0
62 stars 41 forks source link

feat: list instances for defs also #128

Closed alexjbest closed 1 year ago

alexjbest commented 1 year ago

Some defs such as Lean.RBTree have instances, this PR adds the "Instances For" dropdown for defs also so we can see them in docs: e.g. in this case this displays as

def [Lean.RBTree](http://localhost:1000/Lean/Data/RBTree.html#Lean.RBTree) (α : [Type](http://localhost:1000/foundational_types.html) u) (cmp : α → α → [Ordering](http://localhost:1000/Init/Data/Ord.html#Ordering)) :
[Type](http://localhost:1000/foundational_types.html) u
Equations
Instances For

    [Lean.instInhabitedRBTree](http://localhost:1000/Lean/Data/RBTree.html#Lean.instInhabitedRBTree)
    [Lean.instEmptyCollectionRBTree](http://localhost:1000/Lean/Data/RBTree.html#Lean.instEmptyCollectionRBTree)
    [Lean.RBTree.instForInRBTree](http://localhost:1000/Lean/Data/RBTree.html#Lean.RBTree.instForInRBTree)
    [Lean.RBTree.instReprRBTree](http://localhost:1000/Lean/Data/RBTree.html#Lean.RBTree.instReprRBTree)

The downside of this PR is that many defs don't have instances for them, perhaps hiding the instances for dropdown if the list is empty somehow would be better long term

hargoniX commented 1 year ago

The hiding instances if they are empty part does sound useful, the instance stuff is dynamically rendered in the JS so it should be a change there if you want to make it.

alexjbest commented 1 year ago

Yeah Ok, its good to know you think its doable client side, I wasn't sure. I might have a try at making that change sometime then, but probably won't get around to that this week.