lean4-htt/src/Init/Data/Range
Rob23oba e148871087
chore: fix spelling errors (#9175)
(Almost) only typos in constant names and doc-strings were considered;
grammar was not considered. Also, along others,
`mkDefinitionValInferrringUnsafe` has been fixed :-)
2025-07-24 23:35:32 +00:00
..
Polymorphic chore: fix spelling errors (#9175) 2025-07-24 23:35:32 +00:00
Basic.lean feat: make private the default in module (#9044) 2025-06-28 16:30:53 +00:00
Lemmas.lean feat: make private the default in module (#9044) 2025-06-28 16:30:53 +00:00
Polymorphic.lean refactor: replace some Subarray functions with generic slice functions (#9017) 2025-07-03 19:33:19 +00:00