Apply suggestions from code review

leanprover · May 24, 2024 · 3a02c5b · 3a02c5b
1 parent faea640
commit 3a02c5b
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/Lean/Elab/DefView.lean b/src/Lean/Elab/DefView.lean
@@ -84,7 +84,7 @@ instance : Language.ToSnapshotTree HeaderProcessedSnapshot where
 /-- State before elaboration of a mutual definition. -/
 structure DefParsed where
   /--
-  Unstructured syntax object compromising the full "header" of the definition from the modifiers
+  Unstructured syntax object comprising the full "header" of the definition from the modifiers
   (incl. docstring) up to the value, used for determining header elaboration reuse.
   -/
   fullHeaderRef : Syntax
@@ -107,7 +107,7 @@ structure DefView where
   kind          : DefKind
   ref           : Syntax
   /--
-  An unstructured syntax object that compromises the "header" of the definition, i.e. everything up
+  An unstructured syntax object that comprises the "header" of the definition, i.e. everything up
   to the value. Used as a more specific ref for header elaboration.
   -/
   headerRef     : Syntax