During a meeting, it was mentioned that the difference between terms of type bool and formulae (aka type prop) is a bit unclear.
In particular, the Gospel type-checker converts on the fly between both kinds when required, see for instance what is done at 1 and 2. The comment “favor prop over bool” at 3 adds to my confusion.
So I wonder whether the applications where keeping the distinction between bool and prop is important are working with the type-checker as it is now.
During a meeting, it was mentioned that the difference between terms of type
booland formulae (aka typeprop) is a bit unclear.In particular, the Gospel type-checker converts on the fly between both kinds when required, see for instance what is done at 1 and 2. The comment “favor prop over bool” at 3 adds to my confusion.
So I wonder whether the applications where keeping the distinction between
boolandpropis important are working with the type-checker as it is now.