Lean Kernel Arena / tutorial/081_listRecReduction

Test "tutorial/081_listRecReduction"

Expected: 馃憤 accept 路 Size: 17.5鈥疜B 路 Lines: 335 路 lean4export: 3.1.0 路 Lean: 4.34.1 路 馃搫 Declaration 路 馃敆 Source

Reduction behavior of List.rec

Checker Result 鈴憋笍 馃
sokonanoda 馃憤 1鈥痬s 40.0鈥疢B
mathgraph 馃憤 1鈥痬s 37.7鈥疢B
nanoclo 馃憤 1鈥痬s 53.6鈥疢B
con-ron 馃憤 24鈥痬s 60.8鈥疢B
nanobruijn 馃憤 1鈥痬s 11.9鈥疢B
nanoda 馃憤 1鈥痬s 3.2鈥疢B
lazylean 馃憤 1鈥痬s 21.8鈥疢B
con-leche 馃憤 5鈥痬s 22.4鈥疢B
eink0rn 馃憤 2鈥痬s 12.8鈥疢B
official 馃憤 29鈥痬s 65.9鈥疢B
ind-models 馃憤 109鈥痬s 107.8鈥疢B
lean4lean 馃憤 29鈥痬s 96.6鈥疢B
tenet 馃憤 134鈥痬s 45.0鈥疢B
tenet-hs 馃憤 2鈥痬s 10.7鈥疢B
lean4cobol 馃憤 14鈥痬s 13.8鈥疢B
evmlean 馃憤 9.0鈥痵 310.0鈥疢B
mini 馃憤 44鈥痬s 73.6鈥疢B
overfull 馃憤 1.1鈥痬 48.4鈥疢B
metalean-slow 馃憤 83鈥痬s 73.3鈥疢B
tenet-jvm 馃憤 126鈥痬s 65.3鈥疢B
nanoclo-fortran 馃憤 2鈥痬s 4.6鈥疢B
kiota 馃憤 1鈥痬s 9.3鈥疢B
metalean-fast 馃憤 32鈥痬s 73.8鈥疢B
canonical-min 馃憤 390鈥痬s 1.1鈥疓B
rpylean 馃憤 1鈥痬s 5.0鈥疢B
vow-lean-kernel 馃憤 110鈥痬s 8.7鈥疢B
parse-only 馃憤 28鈥痬s 65.7鈥疢B