max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: reduce test size

Browse source 
TODO: investigate why there is a stack overflow in the CI.
I didn't manage to reproduce it on my machine.
This commit is contained in:
Leonardo de Moura 2022-07-04 13:58:06 -07:00
parent ffc90f6a35
commit 2061c9bbea
1 changed files with 1 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
tests/lean/run/finLit.lean
View file

@ -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