From 642418bfda60577db60dfcf828cb6a4f369957da Mon Sep 17 00:00:00 2001 From: Shiney Date: Wed, 25 Oct 2023 21:46:18 +0100 Subject: [PATCH] Fix creation of Trans instance in calculational proof section Two issues, If you use the code as written it doesn't have the right type for Trans, also there's a clash with the existing | operator --- quantifiers_and_equality.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/quantifiers_and_equality.md b/quantifiers_and_equality.md index a092eb9..35278e5 100644 --- a/quantifiers_and_equality.md +++ b/quantifiers_and_equality.md @@ -480,7 +480,7 @@ small example demonstrates how to extend the `calc` notation using new `Trans` i def divides (x y : Nat) : Prop := ∃ k, k*x = y -def divides_trans (h₁ : divides x y) (h₂ : divides y z) : divides x z := +def divides_trans {x y z : Nat} (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₂]⟩ @@ -497,7 +497,7 @@ example (h₁ : divides x y) (h₂ : y = z) : divides x (2*z) := _ = z := h₂ divides _ (2*z) := divides_mul .. -infix:50 " ∣ " => divides +infix:50 (priority := high) " ∣ " => divides example (h₁ : divides x y) (h₂ : y = z) : divides x (2*z) := calc