chore: improve doc string

leanprover · Jan 9, 2025 · c5282db · c5282db
1 parent de2f4e2
commit c5282db
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Init/Grind/Offset.lean b/src/Init/Grind/Offset.lean
@@ -126,7 +126,7 @@ theorem Cnstrs.unsat' (ctx : Context) (c : Cnstrs) : c.isFalse = true → ¬ c.d
   have := Cnstr.of_isFalse ctx h₁
   contradiction
 
-/-- Returns `c_1 → ... → c_n → C -/
+/-- `denote ctx [c_1, ..., c_n] C` is `c_1.denote ctx → ... → c_n.denote ctx → C` -/
 def Cnstrs.denote (ctx : Context) (cs : Cnstrs) (C : Prop) : Prop :=
   match cs with
   | [] => C