CODEWITHSUNDEEP
lean
alagris
alagris

Reputation: 2206

disjunction commutativity in Lean 4

I see

theorem And.comm : a ∧ b ↔ b ∧ a := by
  constructor <;> intro ⟨h₁, h₂⟩ <;> exact ⟨h₂, h₁⟩

in Core.lean but there is no Or.comm to be seen. Where can I find it?

Upvotes: 1

Views: 192

Answers (1)

Alex J Best
Alex J Best

Reputation: 326

The website mathlib4 docs (https://leanprover-community.github.io/mathlib4_docs/) is currently one of the better ways to answer this sort of question, even if you aren't using mathlib4 and only want core Lean.

In this case there is a declaration Or.comm in the Lean 4 standard library (std), see https://leanprover-community.github.io/mathlib4_docs/Std/Logic.html#Or.comm, which probably means it isn't in core. Using Std should be a relatively lightweight addition to your project, and should contain many of these small useful things that aren't in core but possibly could be.

Upvotes: 1

Related Questions