From 9e6534600a583302790c1048d5e4b9776c55a710 Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Thu, 5 Dec 2024 13:53:09 -0800 Subject: [PATCH] mention new file --- CHANGES.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index ce10eac5..8db8b405 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -12,8 +12,9 @@ polymporphically, and (except reverse and zip) all take a function as an argument. SBV firstifies these functions, and the resulting code is compatible with Z3 and CVC5. (Firstification might change in the future, as SMTLib gains support for more higher-order features itself.) Proof-support in backend solvers - for higher-order functions is still quite weak, though KnuckleDragger makes things easier. See - Documentation.SBV.Examples.KnuckleDragger.Lists for several examples. + for higher-order functions is still quite weak, though KnuckleDragger makes things easier. + + * New examples added: Documentation.SBV.Examples.KnuckleDragger.{Lists|EquationalReasoning}. * [BACKWARDS COMPATIBILITY] Removed rarely used functions mapi, foldli, foldri from Data.SBV.List. These can now be defined by the user as we have proper support for fold and map using lambdas.