From 49acdc18b2d5ab2e645876dd06604d170eed0a89 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Fri, 22 Nov 2024 15:37:01 +0000 Subject: [PATCH] refactor: Lint --- HepLean/FeynmanDiagrams/Wick/Contract.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/HepLean/FeynmanDiagrams/Wick/Contract.lean b/HepLean/FeynmanDiagrams/Wick/Contract.lean index c3c781a..8037e4c 100644 --- a/HepLean/FeynmanDiagrams/Wick/Contract.lean +++ b/HepLean/FeynmanDiagrams/Wick/Contract.lean @@ -359,7 +359,7 @@ def Level {n : β„•} {c : Fin n β†’ 𝓔} (str : WickString c final) (k : β„•) : Ξ£ (b1 : Fin k β†’ Fin n) (b2 : Fin k β†’ Fin n), WickContract str b1 b2 /-- There is a finite number of Wick contractions with no contractions. In particular, - this is just the original Wick string. -/ + this is just the original Wick string. -/ instance levelZeroFintype {n : β„•} {c : Fin n β†’ 𝓔} (str : WickString c final) : Fintype (Level str 0) where elems := {⟨Fin.elim0, Fin.elim0, WickContract.string⟩}