From a670de93cd7c06298d00ac6a7872b4df2d5985b6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 13 Aug 2020 14:59:37 -0700
Subject: [PATCH] chore: fix test

---
 tests/lean/run/depElim1.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/lean/run/depElim1.lean b/tests/lean/run/depElim1.lean
index dc95dd3b4a..21beab850b 100644
--- a/tests/lean/run/depElim1.lean
+++ b/tests/lean/run/depElim1.lean
@@ -66,7 +66,7 @@ partial def mkPattern : Expr → MetaM Pattern
     ps ← ps.toList.mapM mkPattern;
     pure $ Pattern.arrayLit type ps
   else match e.arrayLit? with
-    | some es => do
+    | some (_, es) => do
       pats ← es.mapM mkPattern;
       type ← inferType e;
       type ← whnfD type;
@@ -99,7 +99,7 @@ partial def decodeAltLHS (e : Expr) : MetaM AltLHS :=
 forallTelescopeReducing e fun args body => do
   decls ← args.toList.mapM (fun arg => getLocalDecl arg.fvarId!);
   pats  ← decodePats body;
-  pure { fvarDecls := decls, patterns := pats }
+  pure { localDecls := decls, patterns := pats }
 
 partial def decodeAltLHSs : Expr → MetaM (List AltLHS)
 | e =>