simplify docs

LeventErkok · Sep 5, 2024 · e3d0394 · e3d0394
1 parent 6342796
commit e3d0394
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 11 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -8,11 +8,7 @@
   * Add Data.SBV.Tools.KnuckleDragger, inspired by and modeled after Philip Zucker's tool
     by the same name: https://github.com/philzook58/knuckledragger.
 
-  * Added several KnuckleDragger proof examples, under Documentation.SBV.Examples.KnuckleDragger:
-      - Kleene           : Proves kleene algebra theorems
-      - Induction        : Some induction examples
-      - Lists            : Several proofs about lists
-      - Sqrt2IsIrrational: Prove that sqrt(2) is irrational
+  * Added several KnuckleDragger proof examples, see Documentation.SBV.Examples.KnuckleDragger modules.
 
   * Add sDivides, which takes a concrete integer and a (possibly symbolic), and returns sTrue
     if the first argument divides the second. It is essentially equivalent to @a `sMod` n .== 0`,

diff --git a/Data/SBV/Tools/KnuckleDragger.hs b/Data/SBV/Tools/KnuckleDragger.hs
@@ -10,12 +10,7 @@
 -- Inspired by and modeled after Philip Zucker's tool with the same
 -- name, see <http://github.com/philzook58/knuckledragger>.
 --
--- Example uses:
---
---    * Proving Kleene algebra properties: "Documentation.SBV.Examples.KnuckleDragger.Kleene"
---    * Several induction examples: "Documentation.SBV.Examples.KnuckleDragger.Induction"
---    * Sample list properties: "Documentation.SBV.Examples.KnuckleDragger.Lists"
---    * Proving square-root-of-2 is irrational: "Documentation.SBV.Examples.KnuckleDragger.Sqrt2IsIrrational"
+-- See the directory Documentation.SBV.Examples.KnuckleDragger for various examples.
 -----------------------------------------------------------------------------
 
 {-# LANGUAGE ConstraintKinds        #-}