Def readJsonFile

Modification history

2023-11-19 18:46

scripts/runMathlibLinter.lean

chore: use Std's runLinter (#8461)

Deleted readJsonFile View on Github →

2023-07-21 16:03

scripts/checkYaml.lean

feat: port yaml files from mathlib3 (#6026) …

Added readJsonFile View on Github →

2022-06-13 18:50

scripts/runLinter.lean

perf: compile runLinter.lean (#285) …

Added readJsonFile View on Github →