Zulip Chat Archive
Stream: lean4
Topic: How to port to Lean 4 some Lean-3 expression
YurySerdyuk (Oct 09 2024 at 11:57):
Hi !
How to port to Lean 4 expression like
theorem trans {l₁ l₂ l₃ : List α} : l₁ ≃ l₂ → l₂ ≃ l₃ → l₁ ≃ l₃
| ⟨x, y⟩ ⟨z, w⟩ := ⟨Subset.trans x z, Subset.trans w y⟩
Lean 4 gives the error to := symbol ...
Ruben Van de Velde (Oct 09 2024 at 11:59):
Try =>
instead of :=
YurySerdyuk (Oct 09 2024 at 12:04):
I have tried this - gives the new error:
"identifier expected" for ⟨x, y⟩ ⟨z, w⟩ - expression
Ruben Van de Velde (Oct 09 2024 at 12:07):
Please post a #mwe
YurySerdyuk (Oct 09 2024 at 12:14):
This is full code --
import Mathlib.Data.Set.Lattice
open Set
example (α : Type) (p q : α → Prop) : (∃ x, p x ∨ q x) → ∃ x, q x ∨ p x := by
intro
| ⟨w, Or.inl h⟩ => exact ⟨w, Or.inr h⟩
| ⟨w, Or.inr h⟩ => exact ⟨w, Or.inl h⟩
namespace List
private def equiv (l₁ l₂ : List α) := l₁ ⊆ l₂ ∧ l₂ ⊆ l₁
infix:50 " ≃ " => List.equiv
@[refl, simp] theorem equiv.refl (l : List α) : l ≃ l :=
⟨by simp, by simp⟩
@[symm] theorem equiv.symm {l₁ l₂ : List α} : l₁ ≃ l₂ → l₂ ≃ l₁ :=
And.symm
@[trans] theorem equiv.trans {l₁ l₂ l₃ : List α} : l₁ ≃ l₂ → l₂ ≃ l₃ → l₁ ≃ l₃
| ⟨x, y⟩ ⟨z, w⟩ => ⟨Subset.trans x z, Subset.trans w y⟩
Note, that the example after open Set is working ..
Ruben Van de Velde (Oct 09 2024 at 12:14):
With #backticks, please
Marcus Rossel (Oct 09 2024 at 12:21):
Add a comma between ⟨x, y⟩
and ⟨z, w⟩
.
YurySerdyuk (Oct 09 2024 at 12:23):
Thanks - all is working !
Last updated: May 02 2025 at 03:31 UTC