return to top
source
Sequences are indexed by their element sort, and render as Array α on the Lean side.
Array α