From 2061c9bbea847afd6cd301381c5fb239fb21062f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 4 Jul 2022 13:58:06 -0700
Subject: [PATCH] chore: reduce test size

TODO: investigate why there is a stack overflow in the CI.
I didn't manage to reproduce it on my machine.
---
 tests/lean/run/finLit.lean | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/tests/lean/run/finLit.lean b/tests/lean/run/finLit.lean
index 64c1205790..a32ce1c0bb 100644
--- a/tests/lean/run/finLit.lean
+++ b/tests/lean/run/finLit.lean
@@ -5,7 +5,7 @@ def f : Fin 2 → Nat
 example : f 0 = 5 := rfl
 example : f 1 = 45 := rfl
 
-def g : Fin 15 → Nat
+def g : Fin 11 → Nat
   | 0 => 5
   | 1 => 10
   | 2 => 15
@@ -17,10 +17,6 @@ def g : Fin 15 → Nat
   | 8 => 32
   | 9 => 64
   | 10 => 21
-  | 11 => 0
-  | 12 => 5
-  | 13 => 1
-  | 14 => 4
 
 def h : Fin 15 → Nat
   | 0 => 5