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
240 stars 33 forks source link

Make EqSymbolic derivable #636

Closed LeventErkok closed 1 year ago

LeventErkok commented 1 year ago

Just like mergeable instances, we should be able to automatically make symbolic equality to be derivable too. We should add support for this.