From bae336da87cf8418b96cebf0772b0309322cb1b8 Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Sun, 1 Jun 2025 22:07:57 -0700 Subject: [PATCH] chore: make ToMonoM.State.typeParams an FVarIdHashSet rather than an FVarIdSet (#8581) --- src/Lean/Compiler/LCNF/ToMono.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Compiler/LCNF/ToMono.lean b/src/Lean/Compiler/LCNF/ToMono.lean index 7770a85dc4..421a1b37c3 100644 --- a/src/Lean/Compiler/LCNF/ToMono.lean +++ b/src/Lean/Compiler/LCNF/ToMono.lean @@ -12,7 +12,7 @@ import Lean.Compiler.NoncomputableAttr namespace Lean.Compiler.LCNF structure ToMonoM.State where - typeParams : FVarIdSet := {} + typeParams : FVarIdHashSet := {} noncomputableVars : FVarIdMap Name := {} abbrev ToMonoM := StateRefT ToMonoM.State CompilerM