Match new output

LeventErkok · Sep 9, 2024 · aaf3b83 · aaf3b83
1 parent ed70d6c
commit aaf3b83
Show file tree

Hide file tree

Showing 3 changed files with 0 additions and 11 deletions.
diff --git a/Documentation/SBV/Examples/KnuckleDragger/AppendRev.hs b/Documentation/SBV/Examples/KnuckleDragger/AppendRev.hs
@@ -53,7 +53,6 @@ consApp = lemma "consApp"
 -- We have:
 --
 -- >>> appendAssoc
--- Axiom: List(a).induction                Axiom.
 -- Lemma: consApp                          Q.E.D.
 -- Lemma: appendAssoc                      Q.E.D.
 appendAssoc :: IO Proven
@@ -78,7 +77,6 @@ appendAssoc = do
 --
 -- >>> revApp
 -- Lemma: consApp                          Q.E.D.
--- Axiom: List(a).induction                Axiom.
 -- Lemma: consApp                          Q.E.D.
 -- Lemma: appendAssoc                      Q.E.D.
 -- Chain: revApp_induction_pre
@@ -89,7 +87,6 @@ appendAssoc = do
 --   Lemma: revApp_induction_post.1        Q.E.D.
 --   Lemma: revApp_induction_post.2        Q.E.D.
 -- Lemma: revApp_induction_post            Q.E.D.
--- Axiom: List(a).induction                Axiom.
 -- Lemma: revApp                           Q.E.D. [Modulo: sorry]
 revApp :: IO Proven
 revApp = do
@@ -130,11 +127,9 @@ revApp = do
 -- We have:
 --
 -- >>> reverseReverse
--- Axiom: List(a).induction                Axiom.
 -- Lemma: consApp                          Q.E.D.
 -- Lemma: appendAssoc                      Q.E.D.
 -- Lemma: consApp                          Q.E.D.
--- Axiom: List(a).induction                Axiom.
 -- Lemma: consApp                          Q.E.D.
 -- Lemma: appendAssoc                      Q.E.D.
 -- Chain: revApp_induction_pre
@@ -145,9 +140,7 @@ revApp = do
 --   Lemma: revApp_induction_post.1        Q.E.D.
 --   Lemma: revApp_induction_post.2        Q.E.D.
 -- Lemma: revApp_induction_post            Q.E.D.
--- Axiom: List(a).induction                Axiom.
 -- Lemma: revApp                           Q.E.D. [Modulo: sorry]
--- Axiom: List(a).induction                Axiom.
 -- Lemma: reverseReverse                   Q.E.D. [Modulo: revApp]
 reverseReverse :: IO Proven
 reverseReverse = do

diff --git a/Documentation/SBV/Examples/KnuckleDragger/Induction.hs b/Documentation/SBV/Examples/KnuckleDragger/Induction.hs
@@ -26,7 +26,6 @@ import Data.SBV.Tools.KnuckleDragger
 -- We have:
 --
 -- >>> sumProof
--- Axiom: Nat.induction                    Axiom.
 -- Lemma: sum_correct                      Q.E.D.
 sumProof :: IO Proven
 sumProof = do
@@ -48,7 +47,6 @@ sumProof = do
 -- We have:
 --
 -- >>> sumSquareProof
--- Axiom: Nat.induction                    Axiom.
 -- Lemma: sumSquare_correct                Q.E.D.
 sumSquareProof :: IO Proven
 sumSquareProof = do

diff --git a/Documentation/SBV/Examples/KnuckleDragger/ListLen.hs b/Documentation/SBV/Examples/KnuckleDragger/ListLen.hs
@@ -35,7 +35,6 @@ import qualified Data.SBV.List as SL
 -- We have:
 --
 -- >>> listLengthProof
--- Axiom: List(a).induction                Axiom.
 -- Lemma: length_correct                   Q.E.D.
 listLengthProof :: IO Proven
 listLengthProof = do
@@ -58,7 +57,6 @@ listLengthProof = do
 -- than 5 elements and have 42 in it. We have:
 --
 -- >>> badProof `catch` (\(_ :: SomeException) -> pure ())
--- Axiom: List(a).induction                Axiom.
 -- Lemma: bad
 -- *** Failed to prove bad.
 -- Falsifiable. Counter-example: