Update output

LeventErkok · Sep 9, 2024 · 99c29a2 · 99c29a2
1 parent 16f3085
commit 99c29a2
Show file tree

Hide file tree

Showing 4 changed files with 24 additions and 26 deletions.
diff --git a/Documentation/SBV/Examples/KnuckleDragger/AppendRev.hs b/Documentation/SBV/Examples/KnuckleDragger/AppendRev.hs
@@ -53,7 +53,7 @@ consApp = lemma "consApp"
 -- We have:
 --
 -- >>> appendAssoc
--- Axiom: List(a).induction                Admitted.
+-- Axiom: List(a).induction                Axiom.
 -- Lemma: consApp                          Q.E.D.
 -- Lemma: appendAssoc                      Q.E.D.
 appendAssoc :: IO Proven
@@ -78,10 +78,9 @@ appendAssoc = do
 --
 -- >>> revApp
 -- Lemma: consApp                          Q.E.D.
--- Axiom: List(a).induction                Admitted.
+-- Axiom: List(a).induction                Axiom.
 -- Lemma: consApp                          Q.E.D.
 -- Lemma: appendAssoc                      Q.E.D.
--- Lemma: appendNull                       Q.E.D.
 -- Chain: revApp_induction_pre
 --   Lemma: revApp_induction_pre.1         Q.E.D.
 --   Lemma: revApp_induction_pre.2         Q.E.D.
@@ -90,8 +89,8 @@ 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                Admitted.
--- Sorry: revApp                           Blindly believed.
+-- Axiom: List(a).induction                Axiom.
+-- Lemma: revApp                           Q.E.D. [Modulo: sorry]
 revApp :: IO Proven
 revApp = do
    -- We'll need the consApp and associativity-of-append proof, so get a hold on to them
@@ -131,14 +130,13 @@ revApp = do
 -- We have:
 --
 -- >>> reverseReverse
--- Axiom: List(a).induction                Admitted.
+-- Axiom: List(a).induction                Axiom.
 -- Lemma: consApp                          Q.E.D.
 -- Lemma: appendAssoc                      Q.E.D.
 -- Lemma: consApp                          Q.E.D.
--- Axiom: List(a).induction                Admitted.
+-- Axiom: List(a).induction                Axiom.
 -- Lemma: consApp                          Q.E.D.
 -- Lemma: appendAssoc                      Q.E.D.
--- Lemma: appendNull                       Q.E.D.
 -- Chain: revApp_induction_pre
 --   Lemma: revApp_induction_pre.1         Q.E.D.
 --   Lemma: revApp_induction_pre.2         Q.E.D.
@@ -147,9 +145,9 @@ 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                Admitted.
--- Sorry: revApp                           Blindly believed.
--- Axiom: List(a).induction                Admitted.
+-- 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,7 @@ import Data.SBV.Tools.KnuckleDragger
 -- We have:
 --
 -- >>> sumProof
--- Axiom: Nat.induction                    Admitted.
+-- Axiom: Nat.induction                    Axiom.
 -- Lemma: sum_correct                      Q.E.D.
 sumProof :: IO Proven
 sumProof = do
@@ -48,7 +48,7 @@ sumProof = do
 -- We have:
 --
 -- >>> sumSquareProof
--- Axiom: Nat.induction                    Admitted.
+-- Axiom: Nat.induction                    Axiom.
 -- Lemma: sumSquare_correct                Q.E.D.
 sumSquareProof :: IO Proven
 sumSquareProof = do

diff --git a/Documentation/SBV/Examples/KnuckleDragger/Kleene.hs b/Documentation/SBV/Examples/KnuckleDragger/Kleene.hs
@@ -62,17 +62,17 @@ x <= y = x + y .== y
 -- We have:
 --
 -- >>> kleeneProofs
--- Axiom: par_assoc                        Admitted.
--- Axiom: par_comm                         Admitted.
--- Axiom: par_idem                         Admitted.
--- Axiom: par_zero                         Admitted.
--- Axiom: seq_assoc                        Admitted.
--- Axiom: seq_zero                         Admitted.
--- Axiom: seq_one                          Admitted.
--- Axiom: rdistrib                         Admitted.
--- Axiom: ldistrib                         Admitted.
--- Axiom: unfold                           Admitted.
--- Axiom: least_fix                        Admitted.
+-- Axiom: par_assoc                        Axiom.
+-- Axiom: par_comm                         Axiom.
+-- Axiom: par_idem                         Axiom.
+-- Axiom: par_zero                         Axiom.
+-- Axiom: seq_assoc                        Axiom.
+-- Axiom: seq_zero                         Axiom.
+-- Axiom: seq_one                          Axiom.
+-- Axiom: rdistrib                         Axiom.
+-- Axiom: ldistrib                         Axiom.
+-- Axiom: unfold                           Axiom.
+-- Axiom: least_fix                        Axiom.
 -- Lemma: par_lzero                        Q.E.D.
 -- Lemma: par_monotone                     Q.E.D.
 -- Lemma: seq_monotone                     Q.E.D.

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