corner-cases/proof-param-ok - Lean Kernel Arena

Test "corner-cases/proof-param-ok"

Expected: 👍 accept · Size: 2.9 KB · Lines: 53 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration

Keeps two proof parameters in their declared order in an inductive constructor result.

Checker	Result	⏱️	🧠
logos-kernel	👍	0.406 ms	3.0 MB
nano-lean	👍	0.478 ms	13.8 MB
sokonanoda	👍	0.690 ms	27.7 MB
pestka	👍	0.736 ms	10.7 MB
kefir	👍	0.520 ms	6.1 MB
nanoclo	👍	0.643 ms	45.6 MB
kefir-wasm	👍	107 ms	82.2 MB
con-ron	👍	22.1 ms	37.8 MB
con-agua	👍	18.0 ms	10.8 MB
nanoda	👍	0.489 ms	3.1 MB
lazylean	👍	1.09 ms	21.3 MB
con-leche	👍	3.98 ms	20.8 MB
pestka-wasm	👍	79.8 ms	91.6 MB
tenet-jvm	👍	90.3 ms	63.4 MB
eink0rn	👍	1.32 ms	11.5 MB
official	👍	27.8 ms	65.5 MB
ind-models	👍	103 ms	107.5 MB
lean4lean	👍	27.7 ms	96.6 MB
tenet	👍	124 ms	43.7 MB
tenet-hs	👍	1.15 ms	8.1 MB
ocaml4lean	👍	13.3 ms	22.3 MB
lean4cobol	👍	2.70 ms	13.5 MB
evmlean	👍	1.31 s	274.2 MB
overfull	👍	6.25 s	45.8 MB
vow-lean-kernel	👍	123 ms	14.2 MB
mini	👍	34.0 ms	74.1 MB
canonical-min	🚫	386 ms	1.1 GB
kiota	👍	0.652 ms	9.1 MB
metalean-slow	👍	29.7 ms	70.7 MB
nanobruijn	👍	0.618 ms	9.0 MB
metalean-fast	👍	29.7 ms	71.7 MB
nanoclo-fortran	👍	0.766 ms	4.6 MB
rpylean	👍	0.460 ms	4.0 MB
mathgraph	👍	0.641 ms	33.6 MB
parse-only	👍	27.5 ms	66.1 MB