chore(library/data): update data.md
This commit is contained in:
parent
8967f57818
commit
afcf785f03
1 changed files with 1 additions and 0 deletions
|
@ -15,6 +15,7 @@ Basic types:
|
|||
* [int](int/int.md) : the integers
|
||||
* [rat](rat/rat.md) : the rationals
|
||||
* [pnat](pnat.lean) : the positive natural numbers
|
||||
* [real](real.lean) : the real numbers
|
||||
|
||||
Constructors:
|
||||
|
||||
|
|
Loading…
Reference in a new issue