copilot-theorem 3.16.1 → 3.17

raw patch · 3 files changed

+10/−5 lines, 3 filesdep ~copilot-coredep ~copilot-prettyprinterdep ~what4PVP ok

version bump matches the API change (PVP)

Dependency ranges changed: copilot-core, copilot-prettyprinter, what4

API changes (from Hackage documentation)

Files

• CHANGELOG +5/−0
• copilot-theorem.cabal +4/−4
• src/Copilot/Theorem/What4/Translate.hs +1/−1

@@ -1,3 +1,8 @@+2023-11-07+        * Version bump (3.17). (#466)+        * Relax version constraint on what4. (#461)+        * Replace uses of deprecated functions. (#457)+ 2023-09-07         * Version bump (3.16.1). (#455) 

@@ -14,7 +14,7 @@   <https://copilot-language.github.io>.  -version                   : 3.16.1+version                   : 3.17 license                   : BSD3 license-file              : LICENSE maintainer                : Ivan Perez <ivan.perezdominguez@nasa.gov>@@ -61,10 +61,10 @@                           , random                >= 1.1 && < 1.3                           , transformers          >= 0.5 && < 0.7                           , xml                   >= 1.3 && < 1.4-                          , what4                 >= 1.3 && < 1.5+                          , what4                 >= 1.3 && < 1.6 -                          , copilot-core          >= 3.16.1 && < 3.17-                          , copilot-prettyprinter >= 3.16.1 && < 3.17+                          , copilot-core          >= 3.17 && < 3.18+                          , copilot-prettyprinter >= 3.17 && < 3.18    exposed-modules         : Copilot.Theorem                           , Copilot.Theorem.Prove

@@ -365,7 +365,7 @@   CT.Float -> XFloat <$> WFP.iFloatLitSingle sym a   CT.Double -> XDouble <$> WFP.iFloatLitDouble sym a   CT.Array tp -> do-    elts <- traverse (translateConstExpr sym tp) (CT.arrayelems a)+    elts <- traverse (translateConstExpr sym tp) (CT.arrayElems a)     Some n <- return $ mkNatRepr (genericLength elts)     case isZeroOrGT1 n of       Left Refl -> return XEmptyArray