From 32d22075dc587338ce6cfeb67802865b8724baf5 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Sat, 13 Dec 2025 09:14:04 +0100 Subject: [PATCH] doc: fix docstring of `propagateForallPropUp` (#11645) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR fixes the docstring of `propagateForallPropUp`. It was copy’n’pasta before. --- src/Lean/Meta/Tactic/Grind/ForallProp.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Lean/Meta/Tactic/Grind/ForallProp.lean b/src/Lean/Meta/Tactic/Grind/ForallProp.lean index 5a82dd74f3..666d86a0e5 100644 --- a/src/Lean/Meta/Tactic/Grind/ForallProp.lean +++ b/src/Lean/Meta/Tactic/Grind/ForallProp.lean @@ -19,9 +19,8 @@ import Lean.Meta.Tactic.Grind.SynthInstance public section namespace Lean.Meta.Grind /-- -If `parent` is a projection-application `proj_i c`, -check whether the root of the equivalence class containing `c` is a constructor-application `ctor ... a_i ...`. -If so, internalize the term `proj_i (ctor ... a_i ...)` and add the equality `proj_i (ctor ... a_i ...) = a_i`. +Propagator for dependent forall terms +`forall (h : p), q[h]` where p is a proposition. -/ def propagateForallPropUp (e : Expr) : GoalM Unit := do let .forallE n p q bi := e | return ()