search

leanprover / theorem_proving_in_lean4

Theorem Proving in Lean 4
https://leanprover.github.io/theorem_proving_in_lean4/
Apache License 2.0
164 stars 92 forks source link

Fix: ambiguity with newly introduced divisibility symbol #108

Open MatteoGaetzner opened 8 months ago

MatteoGaetzner commented 8 months ago

In newer lean versions, the divisibility symbol $\mid$ (\mid) is already defined, hence

infix:50 " ∣ " => divides

example (h₁ : divides x y) (h₂ : y = z) : divides x (2*z) :=
  calc
    x ∣ y   := h₁
    _ = z   := h₂
    _ ∣ 2*z := divides_mul ..

results in an ambiguity. So I replaced this symbol with double pipe $|$ (\|) and updated the explanation as to why we use this symbol instead of the canonical divisibility symbol.

MichaelJFishman commented 7 months ago

Thanks! I also ran into this. Your code change fixed it for me.