Open trj2059 opened 5 months ago
The below code from the Quantifiers and Equality chapter gives an "ambiguous, possible interpretations" error for this line: x ∣ y := h₁
x ∣ y := h₁
you can see it if you paste the code into https://live.lean-lang.org/
def divides (x y : Nat) : Prop := ∃ k, k*x = y def divides_trans (h₁ : divides x y) (h₂ : divides y z) : divides x z := let ⟨k₁, d₁⟩ := h₁ let ⟨k₂, d₂⟩ := h₂ ⟨k₁ * k₂, by rw [Nat.mul_comm k₁ k₂, Nat.mul_assoc, d₁, d₂]⟩ def divides_mul (x : Nat) (k : Nat) : divides x (k*x) := ⟨k, rfl⟩ instance : Trans divides divides divides where trans := divides_trans example (h₁ : divides x y) (h₂ : y = z) : divides x (2*z) := calc divides x y := h₁ _ = z := h₂ divides _ (2*z) := divides_mul .. 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 ..
The below code from the Quantifiers and Equality chapter gives an "ambiguous, possible interpretations" error for this line:
x ∣ y := h₁
you can see it if you paste the code into https://live.lean-lang.org/