Merge branch 'develop-forall'. Close #470.

ivanperez-keera · ivanperez-keera · commit 5ee005e223f6 · 2023-12-29T03:31:58.000-08:00
**Description** The Copilot API offers the function `Copilot.Language.Spec.forall`, which future versions of GHC will disallow. To ensure that Copilot keeps working with future versions of the compiler, this function should be renamed. **Type** - Management: change to keep Copilot working with future versions of the language/compiler. **Additional context** The proposal was filed in ghc-proposals/ghc-proposals#281, and subsequently accepted in GHC. Details are also available at: https://downloads.haskell.org/ghc/latest/docs/users_guide/using-warnings.html#ghc-flag--Wforall-identifier. **Requester** - Ivan Perez **Method to check presence of bug** Although not a bug, it is possible to detect the presence of this issue by compiling with GHC >= 9.4. Using `-Werror=forall-identifier` will make the issue become a compile-time error. We cannot yet use a test that will produce a failure (expected) if forall is defined (i.e., with -Werror=forall-keyword) because we have to deprecate the function before we remove it. The following Dockerfile checks that the function forall has been deprecated and that the alterative forAll is offered, in which case prints the message Success: ``` FROM ubuntu:focal RUN apt-get update RUN apt-get install --yes libz-dev RUN apt-get install --yes git RUN apt-get install --yes wget RUN mkdir -p $HOME/.ghcup/bin RUN wget https://downloads.haskell.org/~ghcup/0.1.19.2/x86_64-linux-ghcup-0.1.19.2 -O $HOME/.ghcup/bin/ghcup RUN chmod a+x $HOME/.ghcup/bin/ghcup ENV PATH=$PATH:/root/.ghcup/bin/ ENV PATH=$PATH:/root/.cabal/bin/ RUN apt-get install --yes curl RUN apt-get install --yes gcc g++ make libgmp3-dev SHELL ["/bin/bash", "-c"] RUN ghcup install ghc 9.4 RUN ghcup install cabal 3.2 RUN ghcup set ghc 9.4.8 RUN cabal update SHELL ["/bin/bash", "-c"] CMD git clone $REPO && cd $NAME && git checkout $COMMIT && cd .. \ && cabal v1-sandbox init \ && cabal v1-install alex happy \ && cabal v1-install copilot/**/ \ && ! cabal v1-exec -- runhaskell -Werror=deprecations <<< 'import Copilot.Language (true, forall, theorem); spec = theorem "true" (forall true); main :: IO (); main = pure ();' \ && cabal v1-exec -- runhaskell -Werror=forall-identifier -Werror=deprecations <<< 'import Copilot.Language (true, forAll, theorem); spec = theorem "true" (forAll true); main :: IO (); main = pure ();' \ && echo "Success" ``` Command (substitute variables based on new path after merge): ``` $ docker run -e "REPO=https://github.com/Copilot-Language/copilot" -e "NAME=copilot" -e "COMMIT=<HASH>" -it copilot-verify-470 ``` **Expected result** Running the Dockerfile above prints the message "Success", indicating that the old forall function is deprecated and a new variant is being offered. **Solution implemented** Introduce a new function `forAll` that implements the behavior currently implemented by `forall`. Replace all references of `forall` to point to `forAll`, including occurrences in tests and examples. Deprecate `forall`. **Further notes** None.
diff --git a/copilot-language/CHANGELOG b/copilot-language/CHANGELOG
@@ -1,5 +1,6 @@
-2023-12-17
+2023-12-27
         * Add type annotation to help type inference engine. (#469)
+        * Rename forall to forAll. (#470)
 
 2023-11-07
         * Version bump (3.17). (#466)
diff --git a/copilot-language/src/Copilot/Language.hs b/copilot-language/src/Copilot/Language.hs
@@ -37,6 +37,7 @@ module Copilot.Language
   , arg
   , prop
   , theorem
+  , forAll
   , forall, exists
   ) where
 
diff --git a/copilot-language/src/Copilot/Language/Spec.hs b/copilot-language/src/Copilot/Language/Spec.hs
@@ -27,6 +27,7 @@ module Copilot.Language.Spec
   , Prop (..)
   , prop, properties
   , theorem, theorems
+  , forAll
   , forall, exists
   , extractProp
   , Universal, Existential
@@ -160,9 +161,14 @@ data Prop a where
   Forall :: Stream Bool -> Prop Universal
   Exists :: Stream Bool -> Prop Existential
 
+-- | Universal quantification of boolean streams over time.
+forAll :: Stream Bool -> Prop Universal
+forAll = Forall
+
+{-# DEPRECATED forall "Use forAll instead." #-}
 -- | Universal quantification of boolean streams over time.
 forall :: Stream Bool -> Prop Universal
-forall = Forall
+forall = forAll
 
 -- | Existential quantification of boolean streams over time.
 exists :: Stream Bool -> Prop Existential
diff --git a/copilot-libraries/CHANGELOG b/copilot-libraries/CHANGELOG
@@ -1,5 +1,6 @@
-2023-12-24
+2023-12-27
         * Introduce testing infrastructure for Copilot.Library. (#475)
+        * Replace uses of forall with forAll. (#470)
 
 2023-11-07
         * Version bump (3.17). (#466)
diff --git a/copilot-libraries/tests/Test/Extra.hs b/copilot-libraries/tests/Test/Extra.hs
@@ -43,7 +43,8 @@ import Test.QuickCheck.Monadic (monadicIO, run)
 import           Copilot.Interpret.Eval              (ExecTrace (interpObservers),
                                                       ShowType (Haskell), eval)
 import           Copilot.Language                    (Spec, Stream, Typed,
-                                                      forall, observer, prop)
+                                                      observer, prop)
+import qualified Copilot.Language                    as Copilot
 import qualified Copilot.Language.Operators.Boolean  as Copilot
 import qualified Copilot.Language.Operators.Constant as Copilot
 import qualified Copilot.Language.Operators.Eq       as Copilot
@@ -67,7 +68,7 @@ testWithTheorem gen =
         propName = "prop"
 
         spec :: Spec
-        spec = void $ prop propName $ forall stream
+        spec = void $ prop propName $ Copilot.forAll stream
 
     monadicIO $ run $ checkResult Z3 propName spec expectation
 
diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG
@@ -1,5 +1,6 @@
-2023-12-18
+2023-12-27
         * Introduce testing infrastructure for Copilot.Theorem.What4. (#474)
+        * Replace uses of forall with forAll. (#470)
 
 2023-11-07
         * Version bump (3.17). (#466)
diff --git a/copilot-theorem/examples/BoyerMoore.hs b/copilot-theorem/examples/BoyerMoore.hs
@@ -54,9 +54,9 @@ spec = do
     observer ((P.++) "s" (show k)) s
   observer "maj" maj
 
-  i1 <- prop "i1" (forall $ s1 == 1 && s2 == 1 && s3 == 1 && s4 == 1)
-  theorem "r1" (forall $ maj == 1) $ assume i1 >> induct
-  theorem "OK" (forall $ okWith (arbitraryCst "n") ss maj) induct
+  i1 <- prop "i1" (forAll $ s1 == 1 && s2 == 1 && s3 == 1 && s4 == 1)
+  theorem "r1" (forAll $ maj == 1) $ assume i1 >> induct
+  theorem "OK" (forAll $ okWith (arbitraryCst "n") ss maj) induct
 
   where
     s1 = externW8 "s1" (Just $ repeat 1)
diff --git a/copilot-theorem/examples/Grey.hs b/copilot-theorem/examples/Grey.hs
@@ -22,8 +22,8 @@ greyTick reset = a && b
     b = (not reset) && ([False] ++ a)
 
 spec = do
-  theorem "iResetOk"   (forall $ r ==> (ic == 0)) induct
-  theorem "eqCounters" (forall $ it == gt) $ kinduct 3
+  theorem "iResetOk"   (forAll $ r ==> (ic == 0)) induct
+  theorem "eqCounters" (forAll $ it == gt) $ kinduct 3
 
   where
     ic = intCounter r
diff --git a/copilot-theorem/examples/Incr.hs b/copilot-theorem/examples/Incr.hs
@@ -7,9 +7,9 @@ import Copilot.Theorem
 import Copilot.Theorem.Prover.Z3
 
 spec = do
-  bounds <- prop "bounds" (forall $ x < 255)
-  theorem "gt1" (forall $ x > 1) (assume bounds >> induct)
-  theorem "neq0" (forall $ x /= 0) (assume bounds >> induct)
+  bounds <- prop "bounds" (forAll $ x < 255)
+  theorem "gt1" (forAll $ x > 1) (assume bounds >> induct)
+  theorem "neq0" (forAll $ x /= 0) (assume bounds >> induct)
 
   where
     x :: Stream Word8
diff --git a/copilot-theorem/examples/SerialBoyerMoore.hs b/copilot-theorem/examples/SerialBoyerMoore.hs
@@ -48,8 +48,8 @@ spec = do
   observer "s" s
   observer "j" j
 
-  inRange <- prop "inRange" (forall $ input < 3)
-  theorem "J"  (forall j) $ assume inRange >> induct
+  inRange <- prop "inRange" (forAll $ input < 3)
+  theorem "J"  (forAll j) $ assume inRange >> induct
 
   where
     input = externW64 "in" (Just [1, 1, 2, 1, 2, 2, 1, 2, 2, 1, 2, 1])
diff --git a/copilot-theorem/examples/SphericalWCV.hs b/copilot-theorem/examples/SphericalWCV.hs
@@ -184,41 +184,41 @@ horizontalWCV tvar s v = (norm s <= dthr) || ((dcpa s v <= dthr) && (0 <= tvar s
 
 -- Horizontal symmetry --
 horizSymmetry = do
-  theorem "1a" (forall $ tau s v    ~= tau (neg s) (neg v))     arith
-  theorem "1b" (forall $ tcpa s v   ~= tcpa (neg s) (neg v))    arith
-  theorem "1c" (forall $ taumod s v ~= taumod (neg s) (neg v))  arith
-  theorem "1d" (forall $ tep s v    ~= tep (neg s) (neg v))     arith
+  theorem "1a" (forAll $ tau s v    ~= tau (neg s) (neg v))     arith
+  theorem "1b" (forAll $ tcpa s v   ~= tcpa (neg s) (neg v))    arith
+  theorem "1c" (forAll $ taumod s v ~= taumod (neg s) (neg v))  arith
+  theorem "1d" (forAll $ tep s v    ~= tep (neg s) (neg v))     arith
 
 -- Horizontal ordering --
 horizOrdering = do
-  theorem "2a" (forall $ ((s |*| v) < 0 && norm s > dthr && dcpa s v <= dthr)
+  theorem "2a" (forAll $ ((s |*| v) < 0 && norm s > dthr && dcpa s v <= dthr)
     ==> (tep s v <= taumod s v))
     arith
-  theorem "2b" (forall $ ((s |*| v) < 0 && norm s > dthr && dcpa s v <= dthr)
+  theorem "2b" (forAll $ ((s |*| v) < 0 && norm s > dthr && dcpa s v <= dthr)
     ==> (taumod s v <= tcpa s v))
     arith
-  theorem "2c" (forall $ ((s |*| v) < 0 && norm s > dthr && dcpa s v <= dthr)
+  theorem "2c" (forAll $ ((s |*| v) < 0 && norm s > dthr && dcpa s v <= dthr)
     ==> (tcpa s v <= tau s v))
     arith
 
 -- Symmetry --
 symmetry = do
-  theorem "3a" (forall $ wcv tau s sz v vz    == wcv tau (neg s) (-sz) (neg v) (-vz))
+  theorem "3a" (forAll $ wcv tau s sz v vz    == wcv tau (neg s) (-sz) (neg v) (-vz))
     arith
-  theorem "3b" (forall $ wcv tcpa s sz v vz   == wcv tcpa (neg s) (-sz) (neg v) (-vz))
+  theorem "3b" (forAll $ wcv tcpa s sz v vz   == wcv tcpa (neg s) (-sz) (neg v) (-vz))
     arith
-  theorem "3c" (forall $ wcv taumod s sz v vz == wcv taumod (neg s) (-sz) (neg v) (-vz))
+  theorem "3c" (forAll $ wcv taumod s sz v vz == wcv taumod (neg s) (-sz) (neg v) (-vz))
     arith
-  theorem "3d" (forall $ wcv tep s sz v vz    == wcv tep (neg s) (-sz) (neg v) (-vz))
+  theorem "3d" (forAll $ wcv tep s sz v vz    == wcv tep (neg s) (-sz) (neg v) (-vz))
     arith
 
 -- Inclusion --
 inclusion = do
-  theorem "4i"   (forall $ wcv tau s sz v vz    ==> wcv tcpa s sz v vz)
+  theorem "4i"   (forAll $ wcv tau s sz v vz    ==> wcv tcpa s sz v vz)
     arith
-  theorem "4ii"  (forall $ wcv tcpa s sz v vz   ==> wcv taumod s sz v vz )
+  theorem "4ii"  (forAll $ wcv tcpa s sz v vz   ==> wcv taumod s sz v vz )
     arith
-  theorem "4iii" (forall $ wcv taumod s sz v vz ==> wcv tep s sz v vz)
+  theorem "4iii" (forAll $ wcv taumod s sz v vz ==> wcv tep s sz v vz)
     arith
 
 -- Local convexity --
@@ -235,10 +235,10 @@ locallyConvex tvar = (0 <= t1 && t1 <= t2 && t2 <= t3)
       &&  wcv tvar (sx + t3*vx, sy + t3*vy) (sz + t3*vz) v vz)
 
 localConvexity = do
-  theorem "5a" (forall $ locallyConvex tcpa)        arith
-  theorem "5b" (forall $ locallyConvex taumod)      arith
-  theorem "5c" (forall $ locallyConvex tep)         arith
-  theorem "6"  (P.not (forall $ locallyConvex tau)) arithSat
+  theorem "5a" (forAll $ locallyConvex tcpa)        arith
+  theorem "5b" (forAll $ locallyConvex taumod)      arith
+  theorem "5c" (forAll $ locallyConvex tep)         arith
+  theorem "6"  (P.not (forAll $ locallyConvex tau)) arithSat
 
 arith :: Proof Universal
 arith    = onlyValidity def { nraNLSat = True, debug = False }
diff --git a/copilot-theorem/examples/Trig.hs b/copilot-theorem/examples/Trig.hs
@@ -25,37 +25,37 @@ arithSat = onlySat def { debug = False } dReal
 a ~= b = abs (a - b) < 0.001
 
 spec = do
-  bounds <- prop "bounds" (forall $ bounds)
+  bounds <- prop "bounds" (forAll $ bounds)
 
   -- dReal/metit fails this one.
-  -- theorem "dist_eq"     (forall $ d1 ~= d2)
+  -- theorem "dist_eq"     (forAll $ d1 ~= d2)
   --   $ assume bounds >> arith
-  theorem_ "2sin"           (forall $ (2 * (sin x)) <= 3)
+  theorem_ "2sin"           (forAll $ (2 * (sin x)) <= 3)
     $ assume bounds >> arith
-  theorem_ "sin_cos"        (forall $ ((sin x) ** 2 + (cos x) ** 2) ~= 1)
+  theorem_ "sin_cos"        (forAll $ ((sin x) ** 2 + (cos x) ** 2) ~= 1)
     $ assume bounds >> arith
-  theorem_ "sin_cos_pi"     ( forall $ ((sin x) ** 2 + (cos $ x + pi) ** 2) ~= 1)
+  theorem_ "sin_cos_pi"     ( forAll $ ((sin x) ** 2 + (cos $ x + pi) ** 2) ~= 1)
     $ assume bounds >> arith
-  theorem_ "sin_2pi"        ( forall $ (sin x) ~= (sin $ x + 2 * pi))
+  theorem_ "sin_2pi"        ( forAll $ (sin x) ~= (sin $ x + 2 * pi))
     $ assume bounds >> arith
-  theorem_ "cos_2pi"        ( forall $ (cos x) ~= (cos $ x + 2 * pi))
+  theorem_ "cos_2pi"        ( forAll $ (cos x) ~= (cos $ x + 2 * pi))
     $ assume bounds >> arith
-  theorem_ "sin_eq_cos_pi2" ( forall $ (sin x) ~= (cos $ x - (pi/2)))
+  theorem_ "sin_eq_cos_pi2" ( forAll $ (sin x) ~= (cos $ x - (pi/2)))
     $ assume bounds >> arith
-  theorem_ "x^2_2"          ( forall $ (x ** 2 + 1) >= x)
+  theorem_ "x^2_2"          ( forAll $ (x ** 2 + 1) >= x)
     $ assume bounds >> arith
-  theorem_ "sqrt_x"         ( forall $ (x > 2) ==> ((sqrt x) < x))
+  theorem_ "sqrt_x"         ( forAll $ (x > 2) ==> ((sqrt x) < x))
     $ assume bounds >> arith
 
-  theorem_ "x = y"        (P.not $ forall $ x == y)
+  theorem_ "x = y"        (P.not $ forAll $ x == y)
     $ assume bounds >> arithSat
-  theorem_ "sin_cos_3"    (P.not $ forall $ ((sin x) ** 2 + (cos $ x + 3) ** 2) ~= 1)
+  theorem_ "sin_cos_3"    (P.not $ forAll $ ((sin x) ** 2 + (cos $ x + 3) ** 2) ~= 1)
     $ assume bounds >> arithSat
-  theorem_ "sin_pi"       (P.not $ forall $ (sin x) ~= (sin $ x + pi))
+  theorem_ "sin_pi"       (P.not $ forAll $ (sin x) ~= (sin $ x + pi))
     $ assume bounds >> arithSat
-  theorem_ "sin_eq_cos_3" (P.not $ forall $ (sin x) ~= (cos $ x - (3/2)))
+  theorem_ "sin_eq_cos_3" (P.not $ forAll $ (sin x) ~= (cos $ x - (3/2)))
     $ assume bounds >> arithSat
-  theorem_ "sin_eq_cos"   (P.not $ forall $ (sin x) ~= (cos x))
+  theorem_ "sin_eq_cos"   (P.not $ forAll $ (sin x) ~= (cos x))
     $ assume bounds >> arithSat
 
   where
diff --git a/copilot-theorem/examples/WCV.hs b/copilot-theorem/examples/WCV.hs
@@ -108,41 +108,41 @@ horizontalWCV tvar s v =
 
 -- Horizontal symmetry --
 horizSymmetry = do
-  theorem "1a" (forall $ (tau s v)    ~= (tau (neg s) (neg v)))     arith
-  theorem "1b" (forall $ (tcpa s v)   ~= (tcpa (neg s) (neg v)))    arith
-  theorem "1c" (forall $ (taumod s v) ~= (taumod (neg s) (neg v)))  arith
-  theorem "1d" (forall $ (tep s v)    ~= (tep (neg s) (neg v)))     arith
+  theorem "1a" (forAll $ (tau s v)    ~= (tau (neg s) (neg v)))     arith
+  theorem "1b" (forAll $ (tcpa s v)   ~= (tcpa (neg s) (neg v)))    arith
+  theorem "1c" (forAll $ (taumod s v) ~= (taumod (neg s) (neg v)))  arith
+  theorem "1d" (forAll $ (tep s v)    ~= (tep (neg s) (neg v)))     arith
 
 -- Horizontal ordering --
 horizOrdering = do
-  theorem "2a" (forall $ ((s |*| v) < 0 && (norm s) > dthr && (dcpa s v) <= dthr)
+  theorem "2a" (forAll $ ((s |*| v) < 0 && (norm s) > dthr && (dcpa s v) <= dthr)
     ==> ((tep s v) <= (taumod s v)))
     arith
-  theorem "2b" (forall $ ((s |*| v) < 0 && (norm s) > dthr && (dcpa s v) <= dthr)
+  theorem "2b" (forAll $ ((s |*| v) < 0 && (norm s) > dthr && (dcpa s v) <= dthr)
     ==> ((taumod s v) <= (tcpa s v)))
     arith
-  theorem "2c" (forall $ ((s |*| v) < 0 && (norm s) > dthr && (dcpa s v) <= dthr)
+  theorem "2c" (forAll $ ((s |*| v) < 0 && (norm s) > dthr && (dcpa s v) <= dthr)
     ==> ((tcpa s v) <= (tau s v)))
     arith
 
 -- Symmetry --
 symmetry = do
-  theorem "3a" (forall $ (wcv tau s sz v vz)    == (wcv tau (neg s) (-sz) (neg v) (-vz)))
+  theorem "3a" (forAll $ (wcv tau s sz v vz)    == (wcv tau (neg s) (-sz) (neg v) (-vz)))
     arith
-  theorem "3b" (forall $ (wcv tcpa s sz v vz)   == (wcv tcpa (neg s) (-sz) (neg v) (-vz)))
+  theorem "3b" (forAll $ (wcv tcpa s sz v vz)   == (wcv tcpa (neg s) (-sz) (neg v) (-vz)))
     arith
-  theorem "3c" (forall $ (wcv taumod s sz v vz) == (wcv taumod (neg s) (-sz) (neg v) (-vz)))
+  theorem "3c" (forAll $ (wcv taumod s sz v vz) == (wcv taumod (neg s) (-sz) (neg v) (-vz)))
     arith
-  theorem "3d" (forall $ (wcv tep s sz v vz)    == (wcv tep (neg s) (-sz) (neg v) (-vz)))
+  theorem "3d" (forAll $ (wcv tep s sz v vz)    == (wcv tep (neg s) (-sz) (neg v) (-vz)))
     arith
 
 -- Inclusion --
 inclusion = do
-  theorem "4i"   (forall $ (wcv tau s sz v vz)    ==> (wcv tcpa s sz v vz))
+  theorem "4i"   (forAll $ (wcv tau s sz v vz)    ==> (wcv tcpa s sz v vz))
     arith
-  theorem "4ii"  (forall $ (wcv tcpa s sz v vz)   ==> (wcv taumod s sz v vz ))
+  theorem "4ii"  (forAll $ (wcv tcpa s sz v vz)   ==> (wcv taumod s sz v vz ))
     arith
-  theorem "4iii" (forall $ (wcv taumod s sz v vz) ==> (wcv tep s sz v vz))
+  theorem "4iii" (forAll $ (wcv taumod s sz v vz) ==> (wcv tep s sz v vz))
     arith
 
 -- Local convexity --
@@ -159,10 +159,10 @@ locallyConvex tvar = (0 <= t1 && t1 <= t2 && t2 <= t3)
       &&  (wcv tvar (sx + t3*vx, sy + t3*vy) (sz + t3*vz) v vz))
 
 localConvexity = do
-  theorem "5a" (forall $ locallyConvex tcpa)        arith
-  theorem "5b" (forall $ locallyConvex taumod)      arith
-  theorem "5c" (forall $ locallyConvex tep)         arith
-  theorem "6"  (P.not (forall $ locallyConvex tau)) arithSat
+  theorem "5a" (forAll $ locallyConvex tcpa)        arith
+  theorem "5b" (forAll $ locallyConvex taumod)      arith
+  theorem "5c" (forAll $ locallyConvex tep)         arith
+  theorem "6"  (P.not (forAll $ locallyConvex tau)) arithSat
 
 arith :: Proof Universal
 arith    = onlyValidity def { nraNLSat = True, debug = False }
diff --git a/copilot/CHANGELOG b/copilot/CHANGELOG
@@ -1,6 +1,7 @@
-2023-12-24
+2023-12-27
         * Enable tests for copilot-theorem in CI script. (#474)
         * Enable tests for copilot-libraries in CI script. (#475)
+        * Replace uses of forall with forAll. (#470)
 
 2023-11-07
         * Version bump (3.17). (#466)
diff --git a/copilot/examples/WCV.hs b/copilot/examples/WCV.hs
@@ -151,8 +151,8 @@ horizontalWCV tvar s v =
   (((dcpa s v) <= dthr) && (0 <= (tvar s v)) && ((tvar s v) <= tthr))
 
 spec = do
-  Monad.void $ prop "1a" (forall $ (tau s v) ~= (tau (neg s) (neg v)))
-  -- Monad.void $ prop "3d" (forall $ (wcv tep s sz v vz)    == (wcv tep (neg s) (-sz) (neg v) (-vz)))
+  Monad.void $ prop "1a" (forAll $ (tau s v) ~= (tau (neg s) (neg v)))
+  -- Monad.void $ prop "3d" (forAll $ (wcv tep s sz v vz)    == (wcv tep (neg s) (-sz) (neg v) (-vz)))
 
 main :: IO ()
 main = do
diff --git a/copilot/examples/what4/Arithmetic.hs b/copilot/examples/what4/Arithmetic.hs
@@ -21,22 +21,22 @@ spec = do
       efloat = extern "efloat" Nothing
 
   -- The simplest example involving numbers: equality on constant values.
-  void $ prop "Example 1" (forall ((constant (1 :: Int8)) == (constant 1)))
+  void $ prop "Example 1" (forAll ((constant (1 :: Int8)) == (constant 1)))
 
   -- Testing "a < a + 1". This should fail, because it isn't true.
-  void $ prop "Example 2" (forall (eint8 < (eint8 + 1)))
+  void $ prop "Example 2" (forAll (eint8 < (eint8 + 1)))
 
   -- Adding another condition to the above property to make it true.
-  void $ prop "Example 3" (forall ((eint8 < (eint8 + 1)) || (eint8 == 127)))
+  void $ prop "Example 3" (forAll ((eint8 < (eint8 + 1)) || (eint8 == 127)))
 
   -- Just like the previous example, but with words.
-  void $ prop "Example 4" (forall ((eword8 < (eword8 + 1)) || (eword8 == 255)))
+  void $ prop "Example 4" (forAll ((eword8 < (eword8 + 1)) || (eword8 == 255)))
 
   -- An example with floats.
-  void $ prop "Example 5" (forall ((2 * efloat) == (efloat + efloat)))
+  void $ prop "Example 5" (forAll ((2 * efloat) == (efloat + efloat)))
 
   -- Another example with floats. This fails, because it isn't true.
-  void $ prop "Example 6" (forall ((efloat + 1) /= efloat))
+  void $ prop "Example 6" (forAll ((efloat + 1) /= efloat))
 
 main :: IO ()
 main = do
diff --git a/copilot/examples/what4/Propositional.hs b/copilot/examples/what4/Propositional.hs
diff --git a/copilot/examples/what4/Structs.hs b/copilot/examples/what4/Structs.hs
