DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat: Sort TODOs better (#437)

Browse source 
* feat: Add tags

* feat: Add tags to YML

* refactor: Lint

* feat: Sort TODOs
This commit is contained in:
Joseph Tooby-Smith 2025-04-01 10:18:04 +00:00 • committed by GitHub
parent 91d3f9388d
commit 880bd44cb9
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
scripts/MetaPrograms/TODO_to_yml.lean
View file

@ -180,7 +180,8 @@ unsafe def allTODOs : MetaM (List FullTODOInfo) := do
let todos ← getTodoInfo
let informalTODOs ← allInformalTODO
let all := todos ++ informalTODOs
return (all.qsort (fun x y => x.fileName.toString < y.fileName.toString)).toList
return (all.qsort (fun x y => x.fileName.toString < y.fileName.toString
∨ (x.fileName.toString = y.fileName.toString ∧ x.line < y.line))).toList
unsafe def categoriesToYML : MetaM String := do
let todos ← allTODOs