From 94689ca91f0f6ff4fc5cfc75d31cd3e2a78e714f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 13 Aug 2020 16:55:03 -0700
Subject: [PATCH] chore: fix test

---
 tests/lean/run/meta2.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/tests/lean/run/meta2.lean b/tests/lean/run/meta2.lean
index d988750ee6..89ba7b8bd0 100644
--- a/tests/lean/run/meta2.lean
+++ b/tests/lean/run/meta2.lean
@@ -726,6 +726,8 @@ set_option trace.Meta.isDefEq.delta false
 set_option trace.Meta.isDefEq.assign false
 #eval tst41
 
+set_option pp.all false
+
 def tst42 : MetaM Unit := do
 print "----- tst42 -----";
 t ← mkListLit nat [mkNatLit 1, mkNatLit 2];
@@ -736,7 +738,7 @@ print t;
 check t;
 match t.arrayLit? with
 | some (_, xs) => do
-  check $ pure $ xs.size == 2;
+  check $ pure $ xs.length == 2;
   match (xs.get! 0).natLit?, (xs.get! 1).natLit? with
   | some 1, some 2 => pure ()
   | _, _           => throwOther "nat lits expected"