feat: Feynman Trees for two complex scalars #1491
Annotations
6 errors
|
runLinter on HepLean:
HepLean/FeynmanDiagrams/Wick/Contract.lean#L25
@TwoComplexScalar.WickContract inductive missing documentation string
|
|
runLinter on HepLean:
HepLean/FeynmanDiagrams/Wick/String.lean#L87
TwoComplexScalar.WickStringLast inductive missing documentation string
|
|
runLinter on HepLean:
HepLean/FeynmanDiagrams/Wick/Contract.lean#L51
@TwoComplexScalar.WickContract.boundFst argument 8 a✝¹ : TwoComplexScalar.WickContract
|
|
runLinter on HepLean:
HepLean/FeynmanDiagrams/Wick/Contract.lean#L107
@TwoComplexScalar.WickContract.boundSnd argument 8 a✝¹ : TwoComplexScalar.WickContract
|
|
runLinter on HepLean:
HepLean/FeynmanDiagrams/Wick/Contract.lean#L78
@TwoComplexScalar.WickContract.boundFst_strictMono unnecessary have hsp : ↑s <
|
|
runLinter on HepLean
The process '/usr/bin/env' failed with exit code 1
|
Loading