From b105c006a57438d76bc72733a47c9552bd0cae03 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 6 Mar 2022 07:30:34 -0800
Subject: [PATCH] fix: `PrefixTree` `WellFormed` type
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

`β` is a parameter.
---
 src/Lean/Data/PrefixTree.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Data/PrefixTree.lean b/src/Lean/Data/PrefixTree.lean
index 6f10c4eb76..b10bb576af 100644
--- a/src/Lean/Data/PrefixTree.lean
+++ b/src/Lean/Data/PrefixTree.lean
@@ -64,7 +64,7 @@ partial def foldMatchingM [Monad m] (t : PrefixTreeNode α β) (cmp : α → α
       | some t => find ks t d
   find k t init
 
-inductive WellFormed (cmp : α → α → Ordering) : PrefixTreeNode α β → Prop where
+inductive WellFormed {β} (cmp : α → α → Ordering) : PrefixTreeNode α β → Prop where
   | emptyWff    : WellFormed cmp empty
   | insertWff  {t : PrefixTreeNode α β} {k : List α} {val : β} : WellFormed cmp t → WellFormed cmp (insert t cmp k val)