From 4e8b4e96e9aa50134d1da518cc6ab20fc431a50e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 24 Aug 2022 14:16:26 -0700
Subject: [PATCH] feat: simplify `LCtx`

---
 src/Lean/Compiler/LCNF/LCtx.lean | 13 ++++---------
 1 file changed, 4 insertions(+), 9 deletions(-)

diff --git a/src/Lean/Compiler/LCNF/LCtx.lean b/src/Lean/Compiler/LCNF/LCtx.lean
index e95eb764fb..422dce4f81 100644
--- a/src/Lean/Compiler/LCNF/LCtx.lean
+++ b/src/Lean/Compiler/LCNF/LCtx.lean
@@ -14,32 +14,27 @@ LCNF local context.
 structure LCtx where
   localDecls : Std.HashMap FVarId LocalDecl := {}
   funDecls : Std.HashMap FVarId FunDecl := {}
-  fvarIds : Array FVarId := #[]
   deriving Inhabited
 
 def LCtx.addLocalDecl (lctx : LCtx) (fvarId : FVarId) (binderName : Name) (type : Expr) : LCtx :=
   { lctx with
-    localDecls := lctx.localDecls.insert fvarId (.cdecl 0 fvarId binderName type .default)
-    fvarIds    := lctx.fvarIds.push fvarId }
+    localDecls := lctx.localDecls.insert fvarId (.cdecl 0 fvarId binderName type .default) }
 
 def LCtx.addLetDecl (lctx : LCtx) (fvarId : FVarId) (binderName : Name) (type : Expr) (value : Expr) : LCtx :=
   { lctx with
-    localDecls := lctx.localDecls.insert fvarId (.ldecl 0 fvarId binderName type value true)
-    fvarIds    := lctx.fvarIds.push fvarId }
+    localDecls := lctx.localDecls.insert fvarId (.ldecl 0 fvarId binderName type value true) }
 
 def LCtx.addFunDecl (lctx : LCtx) (funDecl : FunDecl) : LCtx :=
   { lctx with
     localDecls := lctx.localDecls.insert funDecl.fvarId (.cdecl 0 funDecl.fvarId funDecl.binderName funDecl.type .default)
-    funDecls   := lctx.funDecls.insert funDecl.fvarId funDecl
-    fvarIds    := lctx.fvarIds.push funDecl.fvarId }
+    funDecls   := lctx.funDecls.insert funDecl.fvarId funDecl }
 
 /--
 Convert a LCNF local context into a regular Lean local context.
 -/
 def LCtx.toLocalContext (lctx : LCtx) : LocalContext := Id.run do
   let mut result := {}
-  for fvarId in lctx.fvarIds do
-    let localDecl := lctx.localDecls.find? fvarId |>.get!
+  for (_, localDecl) in lctx.localDecls.toArray do
     result := result.addDecl localDecl
   return result