Several property functions were added for Bools

[buzden]

Nats have nice property functions that are e.g. applicable in rewrite (like commutativity, neutral element and so), but Bools do not have such. This PR adds some of such properties for not, && and ||.

[clayrat]

Most of these already exist in https://github.com/idris-lang/Idris-dev/blob/master/libs/contrib/Data/Bool/Extra.idr

[buzden]

Most of these already exist in https://github.com/idris-lang/Idris-dev/blob/master/libs/contrib/Data/Bool/Extra.idr

Oooops. But why they are in extra, but not in prelude?

[clayrat]

I think the general idea is that prelude nowadays is seen as a bit overgrown, so it's better to extract non-essential things like property proofs into base or contrib

[buzden]

I think the general idea is that prelude nowadays is seen as a bit overgrown, so it's better to extract non-essential things like property proofs into base or contrib

The problem is when something in base library seems to need something from the contrib. contrib depends in base but not vice-versa.

Does it mean that such things should also go to the contrib library? Or, maybe, some things should "leak" somehow from the contrib to the base?

[buzden]

It looks like base package is better place for existing module than contrib. I suggested this change in the #4789.