DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor: Lint

Browse source
This commit is contained in:
jstoobysmith 2024-11-19 17:00:02 +00:00
parent 2bc561535a
commit b8aae5ac3f
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
HepLean/FeynmanDiagrams/Instances/TwoComplexScalar.lean
View file

@ -125,7 +125,8 @@ def halfEdgeType {n : ℕ} {c : Fin n → 𝓔} : FeynmanTree c → Type := fun
| join _ _ _ t => t.halfEdgeType
/-- The map taking each half-edge to it's associated vertex. -/
def halfEdgeToVertex {n : ℕ} {c : Fin n → 𝓔} : (T : FeynmanTree c) → T.halfEdgeType → T.vertexType := fun
def halfEdgeToVertex {n : ℕ} {c : Fin n → 𝓔} : (T : FeynmanTree c) →
T.halfEdgeType → T.vertexType := fun
| vertex v => fun _ => ()
| union t1 t2 => Sum.map t1.halfEdgeToVertex t2.halfEdgeToVertex
| join _ _ _ t => t.halfEdgeToVertex