From 4117ceaf84fa85f3582f94499bcdecd2f4d0733f Mon Sep 17 00:00:00 2001
From: JadAbouHawili <jad-abou-hawili@hotmail.com>
Date: Tue, 24 Mar 2026 15:15:23 +0200
Subject: [PATCH] doc: typo fix for strict implicit binder (#13099)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR fixes a typo of implicit binders in doc-strings which was `{{
}}` instead of `⦃ ⦄`
---
 src/Lean/Expr.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index 9b3a71b390..2f18f450fa 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -73,7 +73,7 @@ inductive BinderInfo where
   | default
   /-- Implicit binder annotation, e.g., `{x : α}` -/
   | implicit
-  /-- Strict implicit binder annotation, e.g., `{{ x : α }}` -/
+  /-- Strict implicit binder annotation, e.g., `⦃x : α⦄` -/
   | strictImplicit
   /-- Local instance binder annotation, e.g., `[Decidable α]` -/
   | instImplicit
@@ -107,7 +107,7 @@ def BinderInfo.isImplicit : BinderInfo → Bool
   | BinderInfo.implicit => true
   | _                   => false
 
-/-- Return `true` if the given `BinderInfo` is a strict implicit annotation (e.g., `{{α : Type u}}`) -/
+/-- Return `true` if the given `BinderInfo` is a strict implicit annotation (e.g., `⦃α : Type u⦄`) -/
 def BinderInfo.isStrictImplicit : BinderInfo → Bool
   | BinderInfo.strictImplicit => true
   | _                         => false