Lean Kernel Arena / tutorial/062_emptyRec

Test "tutorial/062_emptyRec"

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

Asserting the type of the generated recursor

Checker Result 鈴憋笍 馃
sokonanoda 馃憤 1鈥痬s 33.8鈥疢B
mathgraph 馃憤 1鈥痬s 31.7鈥疢B
nanoclo 馃憤 1鈥痬s 39.6鈥疢B
con-ron 馃憤 23鈥痬s 58.8鈥疢B
nanobruijn 馃憤 0鈥痬s 3.6鈥疢B
nanoda 馃憤 0鈥痬s 3.0鈥疢B
lazylean 馃憤 1鈥痬s 21.7鈥疢B
con-leche 馃憤 4鈥痬s 20.4鈥疢B
eink0rn 馃憤 1鈥痬s 12.0鈥疢B
official 馃憤 28鈥痬s 65.8鈥疢B
ind-models 馃憤 102鈥痬s 104.6鈥疢B
lean4lean 馃憤 28鈥痬s 96.5鈥疢B
tenet 馃憤 120鈥痬s 44.0鈥疢B
tenet-hs 馃憤 1鈥痬s 8.3鈥疢B
lean4cobol 馃憤 2鈥痬s 13.4鈥疢B
evmlean 馃憤 1.1鈥痵 253.9鈥疢B
mini 馃憤 34鈥痬s 71.3鈥疢B
overfull 馃憤 2.4鈥痵 46.0鈥疢B
metalean-slow 馃憤 30鈥痬s 71.3鈥疢B
tenet-jvm 馃憤 99鈥痬s 64.4鈥疢B
nanoclo-fortran 馃憤 1鈥痬s 4.3鈥疢B
kiota 馃憤 1鈥痬s 7.2鈥疢B
metalean-fast 馃憤 30鈥痬s 71.9鈥疢B
canonical-min 馃憤 386鈥痬s 1.1鈥疓B
rpylean 馃憤 0鈥痬s 4.0鈥疢B
vow-lean-kernel 馃憤 53鈥痬s 8.6鈥疢B
parse-only 馃憤 27鈥痬s 66.2鈥疢B