doc(data/nat/{part_enat, lattice}): update doc string (#16345)

leanprover-community · Sep 4, 2022 · 075b0d2 · 075b0d2
1 parent a3e847c
commit 075b0d2
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 1 deletion.
diff --git a/src/data/nat/lattice.lean b/src/data/nat/lattice.lean
@@ -11,7 +11,6 @@ import order.conditionally_complete_lattice
 In this file we
 
 * define a `conditionally_complete_linear_order_bot` structure on `ℕ`;
-* define a `complete_linear_order` structure on `part_enat`;
 * prove a few lemmas about `supr`/`infi`/`set.Union`/`set.Inter` and natural numbers.
 -/
 

diff --git a/src/data/nat/part_enat.lean b/src/data/nat/part_enat.lean
@@ -20,6 +20,7 @@ The following instances are defined:
 
 * `ordered_add_comm_monoid part_enat`
 * `canonically_ordered_add_monoid part_enat`
+* `complete_linear_order part_enat`
 
 There is no additive analogue of `monoid_with_zero`; if there were then `part_enat` could
 be an `add_monoid_with_top`.