docs(data/fp): Move title comment so that it appears in the markdown (#…

…5222)
leanprover-community · Dec 4, 2020 · 54c13bd · 54c13bd
1 parent 30467f4
commit 54c13bd
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/src/data/fp/basic.lean b/src/data/fp/basic.lean
@@ -2,11 +2,12 @@
 Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
-
-Implementation of floating-point numbers (experimental).
 -/
 import data.rat
 import data.semiquot
+/-!
+# Implementation of floating-point numbers (experimental).
+-/
 
 def int.shift2 (a b : ℕ) : ℤ → ℕ × ℕ
 | (int.of_nat e) := (a.shiftl e, b)