Skip to content

Commit

Permalink
grammar
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em committed Sep 11, 2024
1 parent 298e69e commit 621c875
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/Init/Data/Int/DivMod.lean
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ In early versions of Lean, the typeclasses provided by `/` and `%`
were defined in terms of `tdiv` and `tmod`, and these were named simply as `div` and `mod`.
However we decided it was better to use `ediv` and `emod`,
as they are consistent with the conventions used in SMTLib, Mathlib,
as they are consistent with the conventions used in SMTLib, and Mathlib,
and often mathematical reasoning is easier with these conventions.
At that time, we did not rename `div` and `mod` to `tdiv` and `tmod` (along with all their lemma).
Expand Down

0 comments on commit 621c875

Please sign in to comment.