docs(data/char): add module docstring (#8043)

leanprover-community · Jun 30, 2021 · 3ee436d · 3ee436d
1 parent 8cacd99
commit 3ee436d
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/src/data/char.lean b/src/data/char.lean
@@ -2,8 +2,12 @@
 Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
+-/
+
+/-!
+# More `char` instances
 
-Supplementary theorems about the `char` type.
+This file provides a `linear_order` instance on `char`. `char` is the type of Unicode scalar values.
 -/
 
 instance : linear_order char :=