doc: add missing docstring to a theorem

chabulhwi · Jan 28, 2025 · 9b4930a · 9b4930a
1 parent 7a2535f
commit 9b4930a
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/TPIL/Chapter04/Quantifier.lean b/TPIL/Chapter04/Quantifier.lean
@@ -41,6 +41,7 @@ theorem not_exists_isGodlike : ¬∃ (x : Human), IsGodlike x :=
       (show ¬IsMortal w from not_isMortal_of_isGodlike hw)
         (show IsMortal w from forall_isMortal w))
 
+/-- Every human is not godlike. -/
 theorem not_isGodlike (x : Human) : ¬IsGodlike x :=
   fun h : IsGodlike x ↦ show False from
     (show ¬∃ (x : Human), IsGodlike x from not_exists_isGodlike)