From 12381da57b6d3e42fa6f454d865ffaf8ecc687a8 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Tue, 12 Nov 2024 03:00:02 +0000 Subject: [PATCH] perf: inline the `Decidable (Coprime _ _)` instance (#1036) --- Batteries/Data/Nat/Gcd.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Batteries/Data/Nat/Gcd.lean b/Batteries/Data/Nat/Gcd.lean index 708585f5c3..6bc9f43129 100644 --- a/Batteries/Data/Nat/Gcd.lean +++ b/Batteries/Data/Nat/Gcd.lean @@ -19,7 +19,8 @@ See also `nat.coprime_of_dvd` and `nat.coprime_of_dvd'` to prove `nat.Coprime m /-- `m` and `n` are coprime, or relatively prime, if their `gcd` is 1. -/ @[reducible] def Coprime (m n : Nat) : Prop := gcd m n = 1 -instance (m n : Nat) : Decidable (Coprime m n) := inferInstanceAs (Decidable (_ = 1)) +-- if we don't inline this, then the compiler computes the GCD even if it already has it +@[inline] instance (m n : Nat) : Decidable (Coprime m n) := inferInstanceAs (Decidable (_ = 1)) theorem coprime_iff_gcd_eq_one : Coprime m n ↔ gcd m n = 1 := .rfl