Lean Kernel Arena / corner-cases/eta-rule-k

Test "corner-cases/eta-rule-k"

Expected: 🤷 either · Size: 6.5 KB · Lines: 121 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Function eta between a partially applied recursor with rule K and a free variable. The official kernel does not trigger eta expansion here, but a checker may accept the equality by expanding the functions. See https://github.com/leanprover/lean4/issues/12520 for a discussion; the official kernel may adopt eta-expansion of such partial recursor applications, see https://github.com/leanprover/lean4/pull/15374. The same issue for a structure recursor is corner-cases/eta-rec-struct.

Checker Result ⏱️ 🧠
logos-kernel ✋ 0.446 ms 4.5 MB
nano-lean ✋ 0.534 ms 17.9 MB
sokonanoda ✋ 0.794 ms 27.8 MB
pestka ✋ 0.820 ms 10.7 MB
kefir ✋ 0.748 ms 6.4 MB
nanoclo ✋ 0.742 ms 41.7 MB
kefir-wasm ✋ 118 ms 83.5 MB
con-ron ✋ 22.0 ms 35.7 MB
con-agua ✋ 18.1 ms 10.6 MB
nanoda ✋ 0.655 ms 3.1 MB
lazylean ✋ 1.18 ms 21.2 MB
con-leche ✋ 3.91 ms 20.7 MB
pestka-wasm ✋ 81.7 ms 92.6 MB
tenet-jvm ✋ 114 ms 64.8 MB
eink0rn ✋ 1.53 ms 12.0 MB
official ✋ 29.2 ms 66.8 MB
ind-models ✋ 101 ms 107.8 MB
lean4lean ✋ 72.1 ms 104.3 MB
tenet ✋ 134 ms 44.9 MB
tenet-hs ✋ 1.37 ms 8.6 MB
ocaml4lean ✋ 13.9 ms 23.5 MB
lean4cobol ✋ 4.52 ms 13.7 MB
evmlean ✋ 1.76 s 274.1 MB
overfull ✋ 15.6 s 46.3 MB
vow-lean-kernel ✋ 143 ms 14.6 MB
mini ✋ 35.2 ms 74.2 MB
canonical-min ✋ 387 ms 1.1 GB
kiota ✋ 0.922 ms 9.0 MB
metalean-slow 👍 35.6 ms 71.9 MB
nanobruijn ✋ 0.832 ms 10.7 MB
metalean-fast 👍 30.3 ms 72.5 MB
nanoclo-fortran ✋ 1.01 ms 4.6 MB
rpylean ✋ 0.583 ms 4.2 MB
mathgraph ✋ 0.719 ms 33.6 MB
parse-only 👍 27.7 ms 66.1 MB