From 874aadd7e3cd4d0177cbde367c6a5fbf2db611a1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 17 Jan 2022 17:21:18 -0800
Subject: [PATCH] chore: update `namedPattern` signature

Remark: It is not being used yet.
---
 src/Init/Prelude.lean | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 67c7bf3927..cbe06624fe 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -173,10 +173,8 @@ structure Subtype {α : Sort u} (p : α → Prop) where
 -- TODO: delete
 @[reducible] def namedPatternOld {α : Sort u} (x a : α) : α := a
 
-/-- Auxiliary Declaration used to implement the named patterns `x@p`
-    -- TODO: add proof for `x = a`
--/
-@[reducible] def namedPattern {α : Sort u} (x a : α) : α := a
+/-- Auxiliary Declaration used to implement the named patterns `x@h:p` -/
+@[reducible] def namedPattern {α : Sort u} (x a : α) (h : Eq x a) : α := a
 
 /- Auxiliary axiom used to implement `sorry`. -/
 @[extern "lean_sorry", neverExtract]