From d693a55348598cad3ed0dc5fedaa3efad80daf6d Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Fri, 6 Sep 2024 11:25:38 -0700 Subject: [PATCH] simplify a bit --- Documentation/SBV/Examples/KnuckleDragger/AppendRev.hs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Documentation/SBV/Examples/KnuckleDragger/AppendRev.hs b/Documentation/SBV/Examples/KnuckleDragger/AppendRev.hs index 017dc16b1..b294f62da 100644 --- a/Documentation/SBV/Examples/KnuckleDragger/AppendRev.hs +++ b/Documentation/SBV/Examples/KnuckleDragger/AppendRev.hs @@ -97,7 +97,6 @@ revApp = do -- We'll need the consApp and associativity-of-append proof, so get a hold on to them lconsApp <- consApp lAppendAssoc <- appendAssoc - lAppendNull <- appendNull revApp_induction_pre <- chainLemma "revApp_induction_pre" (\(Forall @"x" (x :: SInteger)) (Forall @"xs" xs) (Forall @"ys" ys) @@ -125,7 +124,7 @@ revApp = do inductQ <- inductionPrinciple2 (q @Integer) sorry "revApp" (\(Forall @"xs" (xs :: SList Integer)) (Forall @"ys" ys) -> reverse (xs ++ ys) .== reverse ys ++ reverse xs) - [revApp_induction_pre, lAppendNull, inductQ, revApp_induction_post] + [revApp_induction_pre, revApp_induction_post, inductQ] -- | @reverse (reverse xs) == xs@ --