From 73717f151f2fa1ff41ff1d7ace5327e3342f84a2 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 12 Feb 2025 10:34:58 +0000
Subject: [PATCH] refactor: typos in doc strings

---
 HepLean/Meta/Basic.lean                                  | 8 ++++++++
 HepLean/PerturbationTheory/FieldSpecification/Basic.lean | 7 +++----
 HepLean/PerturbationTheory/WickContraction/Basic.lean    | 2 +-
 3 files changed, 12 insertions(+), 5 deletions(-)

diff --git a/HepLean/Meta/Basic.lean b/HepLean/Meta/Basic.lean
index 5f3f93a..a269175 100644
--- a/HepLean/Meta/Basic.lean
+++ b/HepLean/Meta/Basic.lean
@@ -171,6 +171,14 @@ def noLemmas : CoreM Nat := do
   let x ← imports.mapM HepLean.Imports.getUserConsts
   x.flatFilterSizeM fun c => return !c.isDef && (← c.name.hasPos)
 
+/-- All docstrings present in HepLean. -/
+def allDocStrings : CoreM (Array String) := do
+  let imports ← HepLean.allImports
+  let x ← imports.mapM HepLean.Imports.getUserConsts
+  let x' := x.flatten
+  let docString ← x'.mapM fun c => Lean.Name.getDocString c.name
+  return docString
+
 /-- Number of definitions without a doc-string. -/
 def noDefsNoDocString : CoreM Nat := do
   let imports ← HepLean.allImports
diff --git a/HepLean/PerturbationTheory/FieldSpecification/Basic.lean b/HepLean/PerturbationTheory/FieldSpecification/Basic.lean
index 2b95607..7a06fe3 100644
--- a/HepLean/PerturbationTheory/FieldSpecification/Basic.lean
+++ b/HepLean/PerturbationTheory/FieldSpecification/Basic.lean
@@ -71,13 +71,13 @@ variable (𝓕 : FieldSpecification)
 
 /-- For a field specification `𝓕`, the inductive type `𝓕.FieldOp` is defined
   to contain the following elements:
-- for every `f` in `𝓕.Field`, element of `e` of `AsymptoticLabel f` and `3`-momentum `p`, an
+- For every `f` in `𝓕.Field`, element of `e` of `AsymptoticLabel f` and `3`-momentum `p`, an
   element labelled `inAsymp f e p` corresponding to an incoming asymptotic field operator
   of the field `f`, of label `e` (e.g. specifying the spin), and momentum `p`.
-- for every `f` in `𝓕.Field`, element of `e` of `PositionLabel f` and space-time position `x`, an
+- For every `f` in `𝓕.Field`, element of `e` of `PositionLabel f` and space-time position `x`, an
   element labelled `position f e x` corresponding to a position field operator of the field `f`,
   of label `e` (e.g. specifying the Lorentz index), and position `x`.
-- for every `f` in `𝓕.Field`, element of `e` of `AsymptoticLabel f` and `3`-momentum `p`, an
+- For every `f` in `𝓕.Field`, element of `e` of `AsymptoticLabel f` and `3`-momentum `p`, an
   element labelled `outAsymp f e p` corresponding to an outgoing asymptotic field operator of the
   field `f`, of label `e` (e.g. specifying the spin), and momentum `p`.
 
@@ -94,7 +94,6 @@ As some intuition, if `f` corresponds to a Weyl-fermion field, then
   once represented in the operator algebra, be proportional to the
   annihilation operator `a†(p, s)`.
 
-This type contains all operators which are related to a field.
 -/
 inductive FieldOp (𝓕 : FieldSpecification) where
   | inAsymp : (Σ f, 𝓕.AsymptoticLabel f) × (Fin 3 → ℝ) → 𝓕.FieldOp
diff --git a/HepLean/PerturbationTheory/WickContraction/Basic.lean b/HepLean/PerturbationTheory/WickContraction/Basic.lean
index 73aa956..72ea7d0 100644
--- a/HepLean/PerturbationTheory/WickContraction/Basic.lean
+++ b/HepLean/PerturbationTheory/WickContraction/Basic.lean
@@ -16,7 +16,7 @@ variable {𝓕 : FieldSpecification}
 /--
 Given a natural number `n`, which will correspond to the number of fields needing
 contracting, a Wick contraction
-is a finite set of pairs of `Fin n` (numbers `0`, …, `n-1`), such that no
+is a finite set of pairs of `Fin n` (numbers `0`, ..., `n-1`), such that no
 element of `Fin n` occurs in more then one pair. The pairs are the positions of fields we
 'contract' together.
 -/