Lean Kernel Arena / tutorial/023_imax2

Test "tutorial/023_imax2"

Expected: 👍 accept · Size: 828 B · Lines: 17 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Type inference for forall using imax

Checker Result ⏱️ 🧠
mathgraph 👍 1 ms 29.7 MB
sokonanoda 👍 1 ms 29.5 MB
nanoclo 👍 1 ms 31.7 MB
con-ron 👍 23 ms 56.7 MB
lazylean 👍 1 ms 21.2 MB
nanoda 👍 0 ms 3.0 MB
nanobruijn 👍 1 ms 3.1 MB
con-leche 👍 3 ms 19.9 MB
eink0rn 👍 1 ms 11.2 MB
ind-models 👍 58 ms 103.7 MB
official 👍 27 ms 65.9 MB
lean4lean 👍 27 ms 96.5 MB
tenet 👍 101 ms 42.8 MB
nanoclo-fortran 👍 1 ms 4.3 MB
lean4cobol 👍 1 ms 13.4 MB
evmlean 👍 508 ms 132.2 MB
mini 👍 34 ms 70.5 MB
overfull 👍 1.7 s 45.5 MB
kiota 👍 1 ms 6.9 MB
canonical-min ✋ 386 ms 1.1 GB
rpylean 👍 0 ms 4.0 MB
vow-lean-kernel 👍 46 ms 8.3 MB
official-v4.28.0 👍 34 ms 72.5 MB
still-nanoda 👍 0 ms 3.2 MB
nyaya 👍 2 ms 8.8 MB
parse-only 👍 27 ms 65.8 MB