Skip to content

Commit be9d882

Browse files
add this
1 parent 12c8d74 commit be9d882

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

Numbers.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,3 +2,4 @@ import Numbers.TypeTheory.typetheory
22
import Numbers.integers
33
import Numbers.rationals
44
import Numbers.rationals_order
5+
import Numbers.real

0 commit comments

Comments
 (0)