Marc Huisinga mhuisi
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| ((1 + 2) + (((3 + 4) + 5) + (6 + (7 + 8)))) + ((9 + 10) + (((11 + 12) + 13) + (14 + (15 + 16)))) | |
| (6 and 7 as well as 14 and 15 fit onto one line) | |
| everywhere non-cumulative: | |
| ((1 | |
| + 2) | |
| + (((3 | |
| + 4) | |
| + 5) | |
| + (6 + (7 |
mhuisi
/ Normalizer.lean
Created
August 7, 2025 14:47
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| def normalize (s : String) : String := Id.run do | |
| let s := s.dropWhile (·.isWhitespace) |>.dropRightWhile (·.isWhitespace) | |
| let lines := s.splitOn "\n" | |
| |>.map (fun s => s.dropWhile (·.isWhitespace) |>.dropRightWhile (·.isWhitespace)) | |
| let mut r := "" | |
| for i in [0:lines.length-1] do | |
| let line := lines[i]! | |
| if line.endsWith "." || line.endsWith ":" then | |
| r := r ++ line ++ "\\n" | |
| else if line == "" then |