LeventErkok/sbv — pull request #90 by brianhuffman (2014-06-20 23:23:04+00:00)
Title: Add kind "KBool" to let us distinguish SMTLib types Bool and BitVec 1.

This avoids generation of non-type-correct SMTLib output for proofs like:
prove $ \x -> (x::SWord1) `shiftL` 1 .== 2*x

Previously, this would generate SMTLib code with nonsense like this:
(let ((s1 (bvshl s0 true)))
instead of
(let ((s1 (bvshl s0 #b1)))