3 ms·
Like 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
by johncolanduoni 5y ago
Like 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.