Def ExportCrossRefs.declLocation

Modification history

2026-07-04 02:49

scripts/export_crossrefs.lean

feat(scripts): export wikidata/stacks/kerodon cross-references as JSON (#40701) …

Added ExportCrossRefs.declLocation View on Github →