From 3749a8ad04f3cfdf011a37513a0591543b892986 Mon Sep 17 00:00:00 2001 From: Rob Lewis Date: Tue, 2 Jun 2015 10:10:53 +1000 Subject: [PATCH] chore(library/data/real): update real.md --- library/data/real/real.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/library/data/real/real.md b/library/data/real/real.md index d9a17fdf8..2acde23a7 100644 --- a/library/data/real/real.md +++ b/library/data/real/real.md @@ -3,4 +3,6 @@ data.real The real numbers. -* [basic](basic.lean) : the reals as a commutative ring \ No newline at end of file +* [basic](basic.lean) : the reals as a commutative ring (constructive) +* [order](order.lean) : the reals as an ordered ring (constructive) +* [division](division.lean) : the reals as a discrete linear ordered field (classical) \ No newline at end of file