Zulip Chat Archive

Stream: mathlib4

Topic: and_self


Kevin Buzzard (Oct 24 2022 at 21:00):

Bleurgh and_self is Proppy in core Lean:

@[simp] theorem and_self (p : Prop) : (p  p) = p := propext ⟨(·.1), fun h => h, h⟩⟩

but that's And not and! What do I call

theorem and_self (b : Bool) : (b && b) = b := by cases b <;> simp

in mathlib4?

Scott Morrison (Oct 24 2022 at 21:02):

Bool.and_self?

Kevin Buzzard (Oct 24 2022 at 21:04):

And can I tell #align that?

Kevin Buzzard (Oct 24 2022 at 21:05):

oh lol it's already there :-)

Scott Morrison (Oct 24 2022 at 21:09):

Yeah, increasingly, grepping for #align.*myWeirdlyNamedTheorem is going to be part of the workflow...


Last updated: Dec 20 2023 at 11:08 UTC