search

LeventErkok / sbv

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
https://github.com/LeventErkok/sbv
Other
242 stars 34 forks source link

Add support for fold #635

Closed LeventErkok closed 1 year ago

LeventErkok commented 1 year ago

z3 now supports seq.foldl. We should add support for this. The function argument can come from a fixed set of collections (i.e., addition, multiplication, etc.) or via addSMTDefinition. I think that should cover most everything.