boolean vs logic operations

Stream: new members

[Henning Dieterichs]

Lean 3 has "∨" for props and "||" for bools (also "/\" vs "&&", "tt" vs "true" and "ff" vs "false"). What is ¬ for bools? Apparently I can mix these operators/consts as I like and lean casts them, but the cast operator scares me when I see it in the goal view. What do you recommend here? It seems like I cannot use true in pattern matching, which supports my idea for not mixing props and bools.

[Johan Commelin]

!

[Johan Commelin]

I would indeed advice to avoid the casting as much as possible

[Henning Dieterichs]

Lean says "invalid expression" when I use "!"

[Johan Commelin]

Hmm, I admit that I never use it.

[Johan Commelin]

bnot is the name of the function.

[Rob Lewis]

The notation needs an import, off the top of my head I don't know what.

[Rob Lewis]

mathlib data.bool suffices.

[Johan Commelin]

import data.bool -- apparently

variable (b : bool)

#check !b

[Henning Dieterichs]

thanks, import data.bool does it!

[Henning Dieterichs]

it is rather counterintuitive that && and || are in global scope, but ! is not

[Rob Lewis]

Once upon a time ! was built in syntax for something different. It probably never made its way to core Lean after that syntax was removed.

[Kevin Buzzard]

What is -> for bools? I couldn't find it last time I looked

[Johan Commelin]

!a || b :grinning: