INNER CODE UNIT · Python
render_table
lean-dojo/TorchLean · scripts/generate_unicode_table.py:119
def render_table(intervals: list[tuple[int, int, int]]) -> str:
"""Render the interval table as a few list literals joined into one array.
A single literal with every interval exceeds the elaborator's recursion
limit, so the table is split into parts of at most `PART_SIZE` entries.
"""
entries = [
f"⟨0x{start:X}, 0x{stop:X}, {flags}⟩" for start, stop, flags in intervals
]
parts = [
entries[index : index + PART_SIZE]
for index in range(0, len(entries), PART_SIZE)
]
blocks: list[str] = []
for index, part in enumerate(parts):
blocks.append(
f"/-- Part {index} of `intervals`, split to stay within elaborator limits. -/\n"
f"def intervalsPart{index} : List Interval := [\n{render_entries(part)}]\n"