From d76d7eb81e1d581bce4465a4e89ab0e7cf5f73ff Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 16 Sep 2024 03:10:07 +0000 Subject: [PATCH] chore: remove duplicate ToExpr Fin instance (#16405) This is already provided in Lean. --- Mathlib/Data/Fin/Basic.lean | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/Mathlib/Data/Fin/Basic.lean b/Mathlib/Data/Fin/Basic.lean index be26efa73e6abc..00b3cad8d677f9 100644 --- a/Mathlib/Data/Fin/Basic.lean +++ b/Mathlib/Data/Fin/Basic.lean @@ -1516,16 +1516,6 @@ protected theorem zero_mul' [NeZero n] (k : Fin n) : (0 : Fin n) * k = 0 := by end Mul -open Qq in -instance toExpr (n : ℕ) : Lean.ToExpr (Fin n) where - toTypeExpr := q(Fin $n) - toExpr := match n with - | 0 => finZeroElim - | k + 1 => fun i => show Q(Fin $n) from - have i : Q(Nat) := Lean.mkRawNatLit i -- raw literal to avoid ofNat-double-wrapping - have : Q(NeZero $n) := haveI : $n =Q $k + 1 := ⟨⟩; by exact q(NeZero.succ) - q(OfNat.ofNat $i) - end Fin set_option linter.style.longFile 1700