All definitions of a structure

Stream: general

[Yaël Dillies]

Similar to how we have a list of all instances of a typeclass in the docs, could we have a list of all definitions of a structure?

[Yaël Dillies]

It would also be great to have a list of all lemmas for Prop-valued structures, although those will probably be very numerous.

[Alex J. Best]

These sound like they might be more appropriate as loogle queries, like you could do
@loogle _ -> FirstOrder.Language.Theory.ModelType _
Instances are registered with an attribute, so someone would have to write some code at least to enable this in the docs, and we'd have to check how much data was added and how fast the download is.

[loogle]

:exclamation: <input>:1:84: unexpected end of input; expected '{'

[Alex J. Best]

https://loogle.lean-fro.org/?q=_+-%3E+FirstOrder.Language.Theory.ModelType+_