max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: Rat.lean docstring: "Mathlib" -> "Batteries" (#7708)

Browse source 
This PR fixes an inaccuracy in a module doc for an internal file.

The "Mathib rational numbers" are actually defined in Batteries now -
someone using Batteries but not Mathlib could potentialy be misled by
this. I think this is an improvement on the docstring.
This commit is contained in:
Alex Meiburg 2025-03-28 10:56:44 -04:00 • committed by GitHub
parent d7f5d9a67a
commit 5fb990fcbd
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Std/Internal/Rat.lean
View file

@ -14,7 +14,7 @@ namespace Internal
/-!
Rational numbers for implementing decision procedures.
We should not confuse them with the Mathlib rational numbers.
We should not confuse them with the Batteries rational numbers, also used by Mathlib.
-/
structure Rat where