3 ms·
Doesn't Liquid Haskell[1] use a SAT solver? [1] https://ucsd-progsys.github.io/liquidhaskell-blog/ https://ucsd-progsys.github.io/liquidhaskell-blog/
by sanity31415 5y ago
Doesn't Liquid Haskell[1] use a SAT solver?
[1] https://ucsd-progsys.github.io/liquidhaskell-blog/ https://ucsd-progsys.github.io/liquidhaskell-blog/
- johncolanduoni 5y agoLike most languages with refinement types it uses an SMT solver (a more general problem), though I’m not sure it uses it for pattern matching. I was thinking of Coq, Agda, Lean, etc. which are full-spectrum dependently typed languages. LiquidHaskell is more specialized, though its automated proof capabilities are much stronger.