Checker "rpylean"
Version: v2026.2.12 · 📄 Declaration · 🔗 Source
rpylean - A Lean type checker written in (R)Python.
80/94
25/42
0
Detailed results
Test "bogus1"
Expected: ✋ reject · Size: 11.4 KB · Lines: 198 · lean4export: 3.1.0 · Lean: 4.29.0-rc1 · 📄 Declaration · 🔗 Source
A clearly bogus proof. Also serves as an example for how to write simple cases.
Test result: ✋ rejected · exit code 1 · wall time: 30 ms · instructions: 21.7 M · max rss memory: 6.2 MB
stdout:
Checking 16 declarations…
stderr:
in thm:
True.intro
has type
True
but is expected to have type
Eq.{1} Nat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))
parsed in 0.003772s, checked in 0.001791s
Test "cedar"
Expected: 👍 accept · Size: 728.6 MB · Lines: 13.4 M · lean4export: 3.1.0 · Lean: 4.26.0 · 📄 Declaration · 🔗 Source
Lean formalization of, and proofs about, Cedar.
Auto-generated documentation is available at https://cedar-policy.github.io/cedar-spec/docs/.
This test case exports the whole Cedar module and as such contains even unused parts Init and
Batteries.
Test result: ✋ rejected · exit code 1 · wall time: 1.1 m · instructions: 275.1 G · max rss memory: 14.0 GB
stdout:
WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72f6d40> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> Building large nat expr for <rbigint object at 0x5555fef48fb0> Building large nat expr for <rbigint object at 0x5555fef949e0> Building large nat expr for <rbigint object at 0x5555fefc3298> Building large nat expr for <rbigint object at 0x5555ff027d30> Building large nat expr for <rbigint object at 0x5555ff05d2b0> Building large nat expr for <rbigint object at 0x5555ff0daa58> Building large nat expr for <rbigint object at 0x5555ff0dbd78> Building large nat expr for <rbigint object at 0x5555ff13b4f0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> Building large nat expr for <rbigint object at 0x555601378770> Building large nat expr for <rbigint object at 0x5556013dced8> Building large nat expr for <rbigint object at 0x55560140e830> Building large nat expr for <rbigint object at 0x5556014852c8> Building large nat expr for <rbigint object at 0x5556014c1d48> Building large nat expr for <rbigint object at 0x5556014e97d8> Building large nat expr for <rbigint object at 0x5556015987d0> Building large nat expr for <rbigint object at 0x555601601958> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> Building large nat expr for <rbigint object at 0x555603cd73d0> Building large nat expr for <rbigint object at 0x555603d1e8c0> Building large nat expr for <rbigint object at 0x555603dae218> Building large nat expr for <rbigint object at 0x555603ddaf68> Building large nat expr for <rbigint object at 0x555603e0f9b8> Building large nat expr for <rbigint object at 0x555603eaea58> Building large nat expr for <rbigint object at 0x555603eafdd8> Building large nat expr for <rbigint object at 0x555603f451f0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> Building large nat expr for <rbigint object at 0x55560621f9a0> Building large nat expr for <rbigint object at 0x55560627fc28> Building large nat expr for <rbigint object at 0x5556062a4f20> Building large nat expr for <rbigint object at 0x555606333688> Building large nat expr for <rbigint object at 0x55560636d178> Building large nat expr for <rbigint object at 0x5556063d3e68> Building large nat expr for <rbigint object at 0x555606401af0> Building large nat expr for <rbigint object at 0x55560649c440> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> Building large nat expr for <rbigint object at 0x5556087373e8> Building large nat expr for <rbigint object at 0x55560877ada0> Building large nat expr for <rbigint object at 0x5556087af670> Building large nat expr for <rbigint object at 0x55560883beb0> Building large nat expr for <rbigint object at 0x555608869748> Building large nat expr for <rbigint object at 0x555608902968> Building large nat expr for <rbigint object at 0x5556089643c8> Building large nat expr for <rbigint object at 0x5556089991f0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72daa70> Building large nat expr for <rbigint object at 0x55560b068ae8> Building large nat expr for <rbigint object at 0x55560b09e368> Building large nat expr for <rbigint object at 0x55560b0cf9d0> Building large nat expr for <rbigint object at 0x55560b15edd0> Building large nat expr for <rbigint object at 0x55560b1994c0> Building large nat expr for <rbigint object at 0x55560b2346e0> Building large nat expr for <rbigint object at 0x55560b235b08> Building large nat expr for <rbigint object at 0x55560b2cf0e8> Building large nat expr for <rbigint object at 0x55560bfc2fb0>
stderr:
in DecidableRel:
fun {α β} r ↦ (a : α) → (b : β) → Decidable (r a b)
has type
{α : Sort u} → {β : Sort v} → (α → ∀ (a.«_@»._internal._hyg.0 : β), Prop) → Sort (max u (max v 1))
but is expected to have type
{α : Sort u} → {β : Sort v} → (α → ∀ (a.«_@»._internal._hyg.0 : β), Prop) → Sort (max (max 1 u) v)
Test "constlevels"
Expected: ✋ reject · Size: 15.3 KB · Lines: 283 · lean4export: 3.1.0 · Lean: 4.29.0-rc2 · 📄 Declaration
Regression test for undefined behavior in lazy_delta_reduction_step in the official kernel
In the function lazy_delta_reduction_step, the official kernel expects unfold_definition
to always succeed. However, if the constant has an incorrect number of level parameters, it
actually fails, which leads to memory corruption in lazy_delta_reduction_step.
This test is to check that the official kernel and also other kernels that closely follow the logic of the official kernel correctly handle this unfolding failure.
The issue in the official kernel was originally reported as https://github.com/leanprover/lean4/issues/10577.
Test result: ✋ rejected · exit code 1 · wall time: 310 ms · instructions: 23.7 M · max rss memory: 6.8 MB
stderr:
RPython traceback: File "rpylean_environment.c", line 3887, in Environment__check_one File "rpylean_objects.c", line 33826, in W_Declaration_type_check File "rpylean_objects.c", line 48979, in DefOrTheorem_type_check File "rpylean_objects.c", line 5634, in W_Let_infer Fatal RPython error: AssertionError
Test "cslib"
Expected: 👍 accept · Size: 1.2 GB · Lines: 22.8 M · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
The Lean Computer Science Library (CSLib).
Test result: ✋ rejected · exit code 1 · wall time: 32.7 s · instructions: 245.3 G · max rss memory: 5.3 GB
stdout:
Building large nat expr for <rbigint object at 0x7ffff6d3b160> Building large nat expr for <rbigint object at 0x7ffff6d3b178> Building large nat expr for <rbigint object at 0x555672418698> Building large nat expr for <rbigint object at 0x7ffff6d3b178> Building large nat expr for <rbigint object at 0x7ffff6d3b160> Building large nat expr for <rbigint object at 0x7ffff6d3b178> Building large nat expr for <rbigint object at 0x5556776c0e30> Building large nat expr for <rbigint object at 0x7ffff6d3b178> Building large nat expr for <rbigint object at 0x7ffff6d3b178> Building large nat expr for <rbigint object at 0x7ffff6d3b178> Building large nat expr for <rbigint object at 0x7ffff6d3b178> Building large nat expr for <rbigint object at 0x7ffff6d3b178> Building large nat expr for <rbigint object at 0x7ffff6d3b178> Building large nat expr for <rbigint object at 0x7ffff6d3b178> Building large nat expr for <rbigint object at 0x7ffff6d3b178>
stderr:
in List.Perm.nodup_iff:
fun {α l₁ l₂} ↦ List.Perm.pairwise_iff.{u_1} α (Ne.{u_1 + 1} α) (Ne.symm.{u_1 + 1} α) l₁ l₂
has type
{α : Type u_1} → {l₁ : List.{u_1} α} → {l₂ : List.{u_1} α} → List.Perm.{u_1} α l₁ l₂ → Iff (List.Pairwise.{u_1} α (Ne.{u_1 + 1} α) l₁) (List.Pairwise.{u_1} α (Ne.{u_1 + 1} α) l₂)
but is expected to have type
{α : Type u_1} → {l₁ : List.{u_1} α} → {l₂ : List.{u_1} α} → List.Perm.{u_1} α l₁ l₂ → Iff (List.Nodup.{u_1} α l₁) (List.Nodup.{u_1} α l₂)
in Multiset.nodup_zero:
fun {α} ↦ List.Pairwise.nil.{u_1} α fun x1.«_@».Init.Data.List.Basic.3805720009._hygCtx._hyg.12 x2.«_@».Init.Data.List.Basic.3805720009._hygCtx._hyg.12 ↦ Ne.{u_1 + 1} α x1.«_@».Init.Data.List.Basic.3805720009._hygCtx._hyg.12 x2.«_@».Init.Data.List.Basic.3805720009._hygCtx._hyg.12
has type
{α : Type u_1} → List.Pairwise.{u_1} α (fun x1.«_@».Init.Data.List.Basic.3805720009._hygCtx._hyg.12 x2.«_@».Init.Data.List.Basic.3805720009._hygCtx._hyg.12 ↦ Ne.{u_1 + 1} α x1.«_@».Init.Data.List.Basic.3805720009._hygCtx._hyg.12 x2.«_@».Init.Data.List.Basic.3805720009._hygCtx._hyg.12) (List.nil.{u_1} α)
but is expected to have type
{α : Type u_1} → Multiset.Nodup.{u_1} α (OfNat.ofNat.{u_1} (Multiset.{u_1} α) 0 (Zero.toOfNat0.{u_1} (Multiset.{u_1} α) (Multiset.instZero.{u_1} α)))
in Multiset.notMem_zero:
fun {α} a ↦ List.not_mem_nil.{u_1} α a
has type
{α : Type u_1} → (a : α) → Not (Membership.mem.{u_1, u_1} α (List.{u_1} α) (List.instMembership.{u_1} α) (List.nil.{u_1} α) a)
but is expected to have type
{α : Type u_1} → (a : α) → Not (Membership.mem.{u_1, u_1} α (Multiset.{u_1} α) (Multiset.instMembership.{u_1} α) (OfNat.ofNat.{u_1} (Multiset.{u_1} α) 0 (Zero.toOfNat0.{u_1} (Multiset.{u_1} α) (Multiset.instZero.{u_1} α))) a)
in List.Nodup.filter:
fun {α} p {l} ↦ List.Pairwise.filter.{u} α (fun x1.«_@».Init.Data.List.Basic.3805720009._hygCtx._hyg.12 x2.«_@».Init.Data.List.Basic.3805720009._hygCtx._hyg.12 ↦ Ne.{u + 1} α x1.«_@».Init.Data.List.Basic.3805720009._hygCtx._hyg.12 x2.«_@».Init.Data.List.Basic.3805720009._hygCtx._hyg.12) l p
has type
{α : Type u} → (p : α → Bool) → {l : List.{u} α} → List.Pairwise.{u} α (fun x1.«_@».Init.Data.List.Basic.3805720009._hygCtx._hyg.12 x2.«_@».Init.Data.List.Basic.3805720009._hygCtx._hyg.12 ↦ Ne.{u + 1} α x1.«_@».Init.Data.List.Basic.3805720009._hygCtx._hyg.12 x2.«_@».Init.Data.List.Basic.3805720009._hygCtx._hyg.12) l → List.Pairwise.{u} α (fun x1.«_@».Init.Data.List.Basic.3805720009._hygCtx._hyg.12 x2.«_@».Init.Data.List.Basic.3805720009._hygCtx._hyg.12 ↦ Ne.{u + 1} α x1.«_@».Init.Data.List.Basic.3805720009._hygCtx._hyg.12 x2.«_@».Init.Data.List.Basic.3805720009._hygCtx._hyg.12) (List.filter.{u} α p l)
but is expected to have type
{α : Type u} → (p : α → Bool) → {l : List.{u} α} → List.Nodup.{u} α l → List.Nodup.{u} α (List.filter.{u} α p l)
in Multiset.mem_coe:
fun {α a l} ↦ Iff.rfl (Membership.mem.{u_1, u_1} α (Multiset.{u_1} α) (Multiset.instMembership.{u_1} α) (Multiset.ofList.{u_1} α l) a)
has type
{α : Type u_1} → {a : α} → {l : List.{u_1} α} → Iff (Membership.mem.{u_1, u_1} α (Multiset.{u_1} α) (Multiset.instMembership.{u_1} α) (Multiset.ofList.{u_1} α l) a) (Membership.mem.{u_1, u_1} α (Multiset.{u_1} α) (Multiset.instMembership.{u_1} α) (Multiset.ofList.{u_1} α l) a)
but is expected to have type
{α : Type u_1} → {a : α} → {l : List.{u_1} α} → Iff (Membership.mem.{u_1, u_1} α (Multiset.{u_1} α) (Multiset.instMembership.{u_1} α) (Multiset.ofList.{u_1} α l) a) (Membership.mem.{u_1, u_1} α (List.{u_1} α) (List.instMembership.{u_1} α) l a)
in Setoid.refl:
fun {α} [inst.«_@».Init.Core.245919020._hygCtx._hyg.7 : Setoid.{u} (BVar [0])] a ↦ Equivalence.refl.{u} α (Setoid.r.{u} α inst.«_@».Init.Core.245919020._hygCtx._hyg.7) (Setoid.iseqv.{u} α inst.«_@».Init.Core.245919020._hygCtx._hyg.7) a
has type
{α : Sort u} → [inst.«_@».Init.Core.245919020._hygCtx._hyg.7 : Setoid.{u} α] → (a : α) → Setoid.r.{u} α inst.«_@».Init.Core.245919020._hygCtx._hyg.7 a a
but is expected to have type
{α : Sort u} → [inst.«_@».Init.Core.245919020._hygCtx._hyg.7 : Setoid.{u} α] → (a : α) → HasEquiv.Equiv.{u, 0} α (instHasEquivOfSetoid.{u} α inst.«_@».Init.Core.245919020._hygCtx._hyg.7) a a
in Setoid.trans:
fun {α} [inst.«_@».Init.Core.4164849533._hygCtx._hyg.7 : Setoid.{u} (BVar [0])] {a} {b c} hab hbc ↦ Equivalence.trans.{u} α (Setoid.r.{u} α inst.«_@».Init.Core.4164849533._hygCtx._hyg.7) (Setoid.iseqv.{u} α inst.«_@».Init.Core.4164849533._hygCtx._hyg.7) a b c hab hbc
has type
{α : Sort u} → [inst.«_@».Init.Core.4164849533._hygCtx._hyg.7 : Setoid.{u} α] → {a : α} → {b : α} → {c : α} → HasEquiv.Equiv.{u, 0} α (instHasEquivOfSetoid.{u} α inst.«_@».Init.Core.4164849533._hygCtx._hyg.7) a b → HasEquiv.Equiv.{u, 0} α (instHasEquivOfSetoid.{u} α inst.«_@».Init.Core.4164849533._hygCtx._hyg.7) b c → Setoid.r.{u} α inst.«_@».Init.Core.4164849533._hygCtx._hyg.7 a c
but is expected to have type
{α : Sort u} → [inst.«_@».Init.Core.4164849533._hygCtx._hyg.7 : Setoid.{u} α] → {a : α} → {b : α} → {c : α} → HasEquiv.Equiv.{u, 0} α (instHasEquivOfSetoid.{u} α inst.«_@».Init.Core.4164849533._hygCtx._hyg.7) a b → HasEquiv.Equiv.{u, 0} α (instHasEquivOfSetoid.{u} α inst.«_@».Init.Core.4164849533._hygCtx._hyg.7) b c → HasEquiv.Equiv.{u, 0} α (instHasEquivOfSetoid.{u} α inst.«_@».Init.Core.4164849533._hygCtx._hyg.7) a c
in Setoid.symm:
fun {α} [inst.«_@».Init.Core.2345006597._hygCtx._hyg.7 : Setoid.{u} (BVar [0])] {a} {b} hab ↦ Equivalence.symm.{u} α (Setoid.r.{u} α inst.«_@».Init.Core.2345006597._hygCtx._hyg.7) (Setoid.iseqv.{u} α inst.«_@».Init.Core.2345006597._hygCtx._hyg.7) a b hab
has type
{α : Sort u} → [inst.«_@».Init.Core.2345006597._hygCtx._hyg.7 : Setoid.{u} α] → {a : α} → {b : α} → HasEquiv.Equiv.{u, 0} α (instHasEquivOfSetoid.{u} α inst.«_@».Init.Core.2345006597._hygCtx._hyg.7) a b → Setoid.r.{u} α inst.«_@».Init.Core.2345006597._hygCtx._hyg.7 b a
but is expected to have type
{α : Sort u} → [inst.«_@».Init.Core.2345006597._hygCtx._hyg.7 : Setoid.{u} α] → {a : α} → {b : α} → HasEquiv.Equiv.{u, 0} α (instHasEquivOfSetoid.{u} α inst.«_@».Init.Core.2345006597._hygCtx._hyg.7) a b → HasEquiv.Equiv.{u, 0} α (instHasEquivOfSetoid.{u} α inst.«_@».Init.Core.2345006597._hygCtx._hyg.7) b a
in Quotient.exact:
fun {α s a b} h ↦ _private.Init.Core.0.Quotient.rel_of_eq.{u} α s (Quotient.mk.{u} α s a) (Quotient.mk.{u} α s b) h
has type
{α : Sort u} → {s : Setoid.{u} α} → {a : α} → {b : α} → Eq.{u} (Quotient.{u} α s) (Quotient.mk.{u} α s a) (Quotient.mk.{u} α s b) → _private.Init.Core.0.Quotient.rel.{u} α s (Quotient.mk.{u} α s a) (Quotient.mk.{u} α s b)
but is expected to have type
{α : Sort u} → {s : Setoid.{u} α} → {a : α} → {b : α} → Eq.{u} (Quotient.{u} α s) (Quotient.mk.{u} α s a) (Quotient.mk.{u} α s b) → HasEquiv.Equiv.{u, 0} α (instHasEquivOfSetoid.{u} α s) a b
in Finsupp.mem_support_iff:
fun {α M} [inst.«_@».Mathlib.Data.Finsupp.Defs.3042139972._hygCtx._hyg.10 : Zero.{u_4} (BVar [0])] {f} ↦ Finsupp.mem_support_toFun.{u_1, u_4} α M inst.«_@».Mathlib.Data.Finsupp.Defs.3042139972._hygCtx._hyg.10 f
has type
{α : Type u_1} → {M : Type u_4} → [inst.«_@».Mathlib.Data.Finsupp.Defs.3042139972._hygCtx._hyg.10 : Zero.{u_4} M] → {f : Finsupp.{u_1, u_4} α M inst.«_@».Mathlib.Data.Finsupp.Defs.3042139972._hygCtx._hyg.10} → (a : α) → Iff (Membership.mem.{u_1, u_1} α (Finset.{u_1} α) (Finset.instMembership.{u_1} α) (Finsupp.support.{u_1, u_4} α M inst.«_@».Mathlib.Data.Finsupp.Defs.3042139972._hygCtx._hyg.10 f) a) (Ne.{u_4 + 1} M (Finsupp.toFun.{u_1, u_4} α M inst.«_@».Mathlib.Data.Finsupp.Defs.3042139972._hygCtx._hyg.10 f a) (OfNat.ofNat.{u_4} M 0 (Zero.toOfNat0.{u_4} M inst.«_@».Mathlib.Data.Finsupp.Defs.3042139972._hygCtx._hyg.10)))
but is expected to have type
{α : Type u_1} → {M : Type u_4} → [inst.«_@».Mathlib.Data.Finsupp.Defs.3042139972._hygCtx._hyg.10 : Zero.{u_4} M] → {f : Finsupp.{u_1, u_4} α M inst.«_@».Mathlib.Data.Finsupp.Defs.3042139972._hygCtx._hyg.10} → {a : α} → Iff (Membership.mem.{u_1, u_1} α (Finset.{u_1} α) (Finset.instMembership.{u_1} α) (Finsupp.support.{u_1, u_4} α M inst.«_@».Mathlib.Data.Finsupp.Defs.3042139972._hygCtx._hyg.10 f) a) (Ne.{u_4 + 1} M (DFunLike.coe.{(max u_1 u_4) + 1, u_1 + 1, u_4 + 1} (Finsupp.{u_1, u_4} α M inst.«_@».Mathlib.Data.Finsupp.Defs.3042139972._hygCtx._hyg.10) α (fun a.«_@»._internal._hyg.0 ↦ M) (Finsupp.instFunLike.{u_1, u_4} α M inst.«_@».Mathlib.Data.Finsupp.Defs.3042139972._hygCtx._hyg.10) f a) (OfNat.ofNat.{u_4} M 0 (Zero.toOfNat0.{u_4} M inst.«_@».Mathlib.Data.Finsupp.Defs.3042139972._hygCtx._hyg.10)))
Unexpected error during type checking
RPython traceback:
File "implement.c", line 25, in main
File "rpylean__rcli.c", line 121, in CLI_main
...
Fatal RPython error: RuntimeError
Test "grind-ring-5"
Expected: 👍 accept · Size: 9.7 MB · Lines: 199.5 k · lean4export: 3.1.0 · Lean: 4.29.0-rc1 · 📄 Declaration · 🔗 Source
A grind tactic test from the Lean 4 test suite.
This produces a theorem with a rather large proof term that needs fast reduction.
Test result: ✋ rejected · exit code 1 · wall time: 1.3 s · instructions: 8.4 G · max rss memory: 321.5 MB
stdout:
Building large nat expr for <rbigint object at 0x7ffff7635ef8> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x555557236290> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635ef8> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x555559bc2188> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635f10>
stderr:
Unexpected error during type checking RPython traceback: File "implement.c", line 25, in main File "rpylean__rcli.c", line 121, in CLI_main ... Fatal RPython error: RuntimeError
Test "init"
Expected: 👍 accept · Size: 307.1 MB · Lines: 6.0 M · lean4export: 3.1.0 · Lean: 4.29.0-rc1 · 📄 Declaration · 🔗 Source
The Init module export from Lean 4 core.
This test contains the fundamental building blocks of Lean 4, including:
- Basic data types (Nat, List, Array, String, etc.)
- Core tactics and syntax
- Foundational mathematical structures
- Essential metaprogramming infrastructure
This is one of the smallest meaningful test cases, making it ideal for initial checker validation and debugging.
Test result: ✋ rejected · exit code 1 · wall time: 2.8 m · instructions: 586.1 G · max rss memory: 14.1 GB
stderr:
in DecidableRel:
fun {α β} r ↦ (a : α) → (b : β) → Decidable (r a b)
has type
{α : Sort u} → {β : Sort v} → (α → ∀ (a.«_@»._internal._hyg.0 : β), Prop) → Sort (max u (max v 1))
but is expected to have type
{α : Sort u} → {β : Sort v} → (α → ∀ (a.«_@»._internal._hyg.0 : β), Prop) → Sort (max (max 1 u) v)
in Std.IterM.TerminationMeasures.Finite.rel_of_yield:
fun {α m β} [inst.«_@».Init.Data.Iterators.Basic.3285472565._hygCtx._hyg.7 : Std.Iterator.{w, w'} (BVar [2]) (BVar [1]) (BVar [0])] {it} {it' out} h ↦ Relation.TransGen.single.{w + 1} (Std.IterM.TerminationMeasures.Finite.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.3285472565._hygCtx._hyg.7) (InvImage.{w + 1, w + 1} (Std.IterM.TerminationMeasures.Finite.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.3285472565._hygCtx._hyg.7) (Std.IterM.{w, w'} α m β) (Std.IterM.IsPlausibleSuccessorOf.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.3285472565._hygCtx._hyg.7) (Std.IterM.TerminationMeasures.Finite.it.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.3285472565._hygCtx._hyg.7)) (Std.IterM.TerminationMeasures.Finite.mk.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.3285472565._hygCtx._hyg.7 it') (Std.IterM.TerminationMeasures.Finite.mk.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.3285472565._hygCtx._hyg.7 it) (Exists.intro.{w + 1} (Std.IterStep.{w + 1, w + 1} (Std.IterM.{w, w'} α m β) β) (fun step ↦ And (Eq.{w + 1} (Option.{w} (Std.IterM.{w, w'} α m β)) (Std.IterStep.successor.{w, w} (Std.IterM.{w, w'} α m β) β step) (Option.some.{w} (Std.IterM.{w, w'} α m β) (Std.IterM.TerminationMeasures.Finite.it.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.3285472565._hygCtx._hyg.7 (Std.IterM.TerminationMeasures.Finite.mk.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.3285472565._hygCtx._hyg.7 it')))) (Std.IterM.IsPlausibleStep.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.3285472565._hygCtx._hyg.7 (Std.IterM.TerminationMeasures.Finite.it.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.3285472565._hygCtx._hyg.7 (Std.IterM.TerminationMeasures.Finite.mk.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.3285472565._hygCtx._hyg.7 it)) step)) (Std.IterStep.yield.{w + 1, w + 1} (Std.IterM.{w, w'} α m β) β it' out) (And.intro (Eq.{w + 1} (Option.{w} (Std.IterM.{w, w'} α m β)) (Std.IterStep.successor.{w, w} (Std.IterM.{w, w'} α m β) β (Std.IterStep.yield.{w + 1, w + 1} (Std.IterM.{w, w'} α m β) β it' out)) (Option.some.{w} (Std.IterM.{w, w'} α m β) (Std.IterM.TerminationMeasures.Finite.it.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.3285472565._hygCtx._hyg.7 (Std.IterM.TerminationMeasures.Finite.mk.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.3285472565._hygCtx._hyg.7 it')))) (Std.IterM.IsPlausibleStep.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.3285472565._hygCtx._hyg.7 (Std.IterM.TerminationMeasures.Finite.it.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.3285472565._hygCtx._hyg.7 (Std.IterM.TerminationMeasures.Finite.mk.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.3285472565._hygCtx._hyg.7 it)) (Std.IterStep.yield.{w + 1, w + 1} (Std.IterM.{w, w'} α m β) β it' out)) (rfl.{w + 1} (Option.{w} (Std.IterM.{w, w'} α m β)) (Std.IterStep.successor.{w, w} (Std.IterM.{w, w'} α m β) β (Std.IterStep.yield.{w + 1, w + 1} (Std.IterM.{w, w'} α m β) β it' out))) h))
has type
{α : Type w} → {m : Type w → Type w'} → {β : Type w} → [inst.«_@».Init.Data.Iterators.Basic.3285472565._hygCtx._hyg.7 : Std.Iterator.{w, w'} α m β] → {it : Std.IterM.{w, w'} α m β} → {it' : Std.IterM.{w, w'} α m β} → {out : β} → Std.IterM.IsPlausibleStep.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.3285472565._hygCtx._hyg.7 it (Std.IterStep.yield.{w + 1, w + 1} (Std.IterM.{w, w'} α m β) β it' out) → Relation.TransGen.{w + 1} (Std.IterM.TerminationMeasures.Finite.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.3285472565._hygCtx._hyg.7) (InvImage.{w + 1, w + 1} (Std.IterM.TerminationMeasures.Finite.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.3285472565._hygCtx._hyg.7) (Std.IterM.{w, w'} α m β) (Std.IterM.IsPlausibleSuccessorOf.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.3285472565._hygCtx._hyg.7) (Std.IterM.TerminationMeasures.Finite.it.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.3285472565._hygCtx._hyg.7)) (Std.IterM.TerminationMeasures.Finite.mk.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.3285472565._hygCtx._hyg.7 it') (Std.IterM.TerminationMeasures.Finite.mk.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.3285472565._hygCtx._hyg.7 it)
but is expected to have type
{α : Type w} → {m : Type w → Type w'} → {β : Type w} → [inst.«_@».Init.Data.Iterators.Basic.3285472565._hygCtx._hyg.7 : Std.Iterator.{w, w'} α m β] → {it : Std.IterM.{w, w'} α m β} → {it' : Std.IterM.{w, w'} α m β} → {out : β} → Std.IterM.IsPlausibleStep.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.3285472565._hygCtx._hyg.7 it (Std.IterStep.yield.{w + 1, w + 1} (Std.IterM.{w, w'} α m β) β it' out) → Std.IterM.TerminationMeasures.Finite.Rel.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.3285472565._hygCtx._hyg.7 (Std.IterM.TerminationMeasures.Finite.mk.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.3285472565._hygCtx._hyg.7 it') (Std.IterM.TerminationMeasures.Finite.mk.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.3285472565._hygCtx._hyg.7 it)
in Std.IterM.TerminationMeasures.Finite.rel_of_skip:
fun {α m β} [inst.«_@».Init.Data.Iterators.Basic.2952397158._hygCtx._hyg.7 : Std.Iterator.{w, w'} (BVar [2]) (BVar [1]) (BVar [0])] {it} {it'} h ↦ Relation.TransGen.single.{w + 1} (Std.IterM.TerminationMeasures.Finite.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.2952397158._hygCtx._hyg.7) (InvImage.{w + 1, w + 1} (Std.IterM.TerminationMeasures.Finite.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.2952397158._hygCtx._hyg.7) (Std.IterM.{w, w'} α m β) (Std.IterM.IsPlausibleSuccessorOf.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.2952397158._hygCtx._hyg.7) (Std.IterM.TerminationMeasures.Finite.it.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.2952397158._hygCtx._hyg.7)) (Std.IterM.TerminationMeasures.Finite.mk.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.2952397158._hygCtx._hyg.7 it') (Std.IterM.TerminationMeasures.Finite.mk.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.2952397158._hygCtx._hyg.7 it) (Exists.intro.{w + 1} (Std.IterStep.{w + 1, w + 1} (Std.IterM.{w, w'} α m β) β) (fun step ↦ And (Eq.{w + 1} (Option.{w} (Std.IterM.{w, w'} α m β)) (Std.IterStep.successor.{w, w} (Std.IterM.{w, w'} α m β) β step) (Option.some.{w} (Std.IterM.{w, w'} α m β) (Std.IterM.TerminationMeasures.Finite.it.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.2952397158._hygCtx._hyg.7 (Std.IterM.TerminationMeasures.Finite.mk.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.2952397158._hygCtx._hyg.7 it')))) (Std.IterM.IsPlausibleStep.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.2952397158._hygCtx._hyg.7 (Std.IterM.TerminationMeasures.Finite.it.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.2952397158._hygCtx._hyg.7 (Std.IterM.TerminationMeasures.Finite.mk.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.2952397158._hygCtx._hyg.7 it)) step)) (Std.IterStep.skip.{w + 1, w + 1} (Std.IterM.{w, w'} α m β) β it') (And.intro (Eq.{w + 1} (Option.{w} (Std.IterM.{w, w'} α m β)) (Std.IterStep.successor.{w, w} (Std.IterM.{w, w'} α m β) β (Std.IterStep.skip.{w + 1, w + 1} (Std.IterM.{w, w'} α m β) β it')) (Option.some.{w} (Std.IterM.{w, w'} α m β) (Std.IterM.TerminationMeasures.Finite.it.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.2952397158._hygCtx._hyg.7 (Std.IterM.TerminationMeasures.Finite.mk.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.2952397158._hygCtx._hyg.7 it')))) (Std.IterM.IsPlausibleStep.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.2952397158._hygCtx._hyg.7 (Std.IterM.TerminationMeasures.Finite.it.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.2952397158._hygCtx._hyg.7 (Std.IterM.TerminationMeasures.Finite.mk.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.2952397158._hygCtx._hyg.7 it)) (Std.IterStep.skip.{w + 1, w + 1} (Std.IterM.{w, w'} α m β) β it')) (rfl.{w + 1} (Option.{w} (Std.IterM.{w, w'} α m β)) (Std.IterStep.successor.{w, w} (Std.IterM.{w, w'} α m β) β (Std.IterStep.skip.{w + 1, w + 1} (Std.IterM.{w, w'} α m β) β it'))) h))
has type
{α : Type w} → {m : Type w → Type w'} → {β : Type w} → [inst.«_@».Init.Data.Iterators.Basic.2952397158._hygCtx._hyg.7 : Std.Iterator.{w, w'} α m β] → {it : Std.IterM.{w, w'} α m β} → {it' : Std.IterM.{w, w'} α m β} → Std.IterM.IsPlausibleStep.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.2952397158._hygCtx._hyg.7 it (Std.IterStep.skip.{w + 1, w + 1} (Std.IterM.{w, w'} α m β) β it') → Relation.TransGen.{w + 1} (Std.IterM.TerminationMeasures.Finite.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.2952397158._hygCtx._hyg.7) (InvImage.{w + 1, w + 1} (Std.IterM.TerminationMeasures.Finite.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.2952397158._hygCtx._hyg.7) (Std.IterM.{w, w'} α m β) (Std.IterM.IsPlausibleSuccessorOf.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.2952397158._hygCtx._hyg.7) (Std.IterM.TerminationMeasures.Finite.it.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.2952397158._hygCtx._hyg.7)) (Std.IterM.TerminationMeasures.Finite.mk.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.2952397158._hygCtx._hyg.7 it') (Std.IterM.TerminationMeasures.Finite.mk.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.2952397158._hygCtx._hyg.7 it)
but is expected to have type
{α : Type w} → {m : Type w → Type w'} → {β : Type w} → [inst.«_@».Init.Data.Iterators.Basic.2952397158._hygCtx._hyg.7 : Std.Iterator.{w, w'} α m β] → {it : Std.IterM.{w, w'} α m β} → {it' : Std.IterM.{w, w'} α m β} → Std.IterM.IsPlausibleStep.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.2952397158._hygCtx._hyg.7 it (Std.IterStep.skip.{w + 1, w + 1} (Std.IterM.{w, w'} α m β) β it') → Std.IterM.TerminationMeasures.Finite.Rel.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.2952397158._hygCtx._hyg.7 (Std.IterM.TerminationMeasures.Finite.mk.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.2952397158._hygCtx._hyg.7 it') (Std.IterM.TerminationMeasures.Finite.mk.{w, w'} α m β inst.«_@».Init.Data.Iterators.Basic.2952397158._hygCtx._hyg.7 it)
Test "init-prelude"
Expected: 👍 accept · Size: 3.5 MB · Lines: 63.5 k · lean4export: 3.1.0 · Lean: 4.29.0-rc1 · 📄 Declaration · 🔗 Source
The Init.Prelude module export.
Test result: ✋ rejected · exit code 1 · wall time: 1.4 s · instructions: 7.1 G · max rss memory: 290.1 MB
stdout:
Building large nat expr for <rbigint object at 0x7ffff74e2140> Building large nat expr for <rbigint object at 0x7ffff74e2158> Building large nat expr for <rbigint object at 0x7ffff510a248> Building large nat expr for <rbigint object at 0x7ffff74e2158> Building large nat expr for <rbigint object at 0x7ffff74e2140> Building large nat expr for <rbigint object at 0x7ffff74e2158> Building large nat expr for <rbigint object at 0x7ffff57f06b0> Building large nat expr for <rbigint object at 0x7ffff74e2158> Building large nat expr for <rbigint object at 0x7ffff74e2158> Building large nat expr for <rbigint object at 0x7ffff74e2158> Building large nat expr for <rbigint object at 0x7ffff74e2158> Building large nat expr for <rbigint object at 0x7ffff74e2158> Building large nat expr for <rbigint object at 0x7ffff74e2158> Building large nat expr for <rbigint object at 0x7ffff74e2158> Building large nat expr for <rbigint object at 0x7ffff74e2158>
stderr:
Unexpected error during type checking RPython traceback: File "implement.c", line 25, in main File "rpylean__rcli.c", line 121, in CLI_main ... Fatal RPython error: RuntimeError
Test "mathlib"
Expected: 👍 accept · Size: 4.9 GB · Lines: 92.5 M · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
The complete Mathlib library export.
This test contains all the mathematical definitions, theorems, and proofs from Mathlib, representing the largest and most comprehensive test case in the Lean kernel arena.
This test is based on a commit that includes https://github.com/leanprover-community/mathlib4/pull/33794 to include the performance fix therein.
Test result: ✋ rejected · exit code 1 · wall time: 3.0 m · instructions: 788.2 G · max rss memory: 14.1 GB
Test "mlir"
Expected: 👍 accept · Size: 28.8 MB · Lines: 576.3 k · lean4export: 3.1.0 · Lean: 4.27.0-nightly-2025-12-01 · 📄 Declaration · 🔗 Source
The main theorems from lean-mlir.
Test result: ✋ rejected · exit code 1 · wall time: 3.2 s · instructions: 19.1 G · max rss memory: 449.5 MB
stdout:
Building large nat expr for <rbigint object at 0x7ffff729a308> Building large nat expr for <rbigint object at 0x7ffff729a2f0> Building large nat expr for <rbigint object at 0x55556f16c038> Building large nat expr for <rbigint object at 0x7ffff729a2f0> Building large nat expr for <rbigint object at 0x7ffff729a308> Building large nat expr for <rbigint object at 0x7ffff729a2f0> Building large nat expr for <rbigint object at 0x555566c7a1d0> Building large nat expr for <rbigint object at 0x7ffff729a2f0> Building large nat expr for <rbigint object at 0x7ffff729a2f0> Building large nat expr for <rbigint object at 0x7ffff729a2f0> Building large nat expr for <rbigint object at 0x7ffff729a2f0> Building large nat expr for <rbigint object at 0x7ffff729a2f0> Building large nat expr for <rbigint object at 0x7ffff729a2f0> Building large nat expr for <rbigint object at 0x7ffff729a2f0> Building large nat expr for <rbigint object at 0x7ffff729a2f0>
stderr:
Unexpected error during type checking RPython traceback: File "implement.c", line 25, in main File "rpylean__rcli.c", line 121, in CLI_main ... Fatal RPython error: RuntimeError
Test "std"
Expected: 👍 accept · Size: 522.7 MB · Lines: 10.0 M · lean4export: 3.1.0 · Lean: 4.29.0-rc1 · 📄 Declaration · 🔗 Source
The complete Std library export from Lean 4.
This test contains the standard library extensions beyond core Lean 4, including:
- Enhanced data structures (HashMap, RBTree, etc.)
- Additional mathematical operations
- Extended list and array operations
- Utility functions and theorems
This represents a medium-sized test case, larger than core modules but smaller than Mathlib, making it useful for performance testing.
Test result: ✋ rejected · exit code 1 · wall time: 2.4 m · instructions: 434.2 G · max rss memory: 14.1 GB
Test "tutorial/001_basicDef"
Expected: 👍 accept · Size: 371 B · Lines: 6 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Basic definition
Test result: 👍 accepted · exit code 0 · wall time: 48 ms · instructions: 19.4 M · max rss memory: 5.8 MB
stdout:
Checking 1 declaration… All declarations are type-correct.
stderr:
parsed in 0.002678s, checked in 0.001527s
Test "tutorial/002_badDef"
Expected: ✋ reject · Size: 369 B · Lines: 6 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Mismatched types
Test result: ✋ rejected · exit code 1 · wall time: 13 ms · instructions: 12.5 M · max rss memory: 5.8 MB
stdout:
Checking 1 declaration…
stderr:
in badDef: Type has type Type 1 but is expected to have type Prop parsed in 0.000684s, checked in 0.000089s
Test "tutorial/003_arrowType"
Expected: 👍 accept · Size: 626 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Arrow type (function type)
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 12.5 M · max rss memory: 5.8 MB
stdout:
Checking 1 declaration… All declarations are type-correct.
stderr:
parsed in 0.000615s, checked in 0.000061s
Test "tutorial/004_dependentType"
Expected: 👍 accept · Size: 464 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Dependent type (forall)
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 12.4 M · max rss memory: 5.8 MB
stdout:
Checking 1 declaration… All declarations are type-correct.
stderr:
parsed in 0.000464s, checked in 0.000029s
Test "tutorial/005_constType"
Expected: 👍 accept · Size: 901 B · Lines: 17 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Lambda expression
Test result: 👍 accepted · exit code 0 · wall time: 6 ms · instructions: 12.7 M · max rss memory: 5.8 MB
stdout:
Checking 1 declaration… All declarations are type-correct.
stderr:
parsed in 0.000474s, checked in 0.000068s
Test "tutorial/006_betaReduction"
Expected: 👍 accept · Size: 1.3 KB · Lines: 27 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Lambda reduction
Test result: 👍 accepted · exit code 0 · wall time: 6 ms · instructions: 12.7 M · max rss memory: 5.9 MB
stdout:
Checking 2 declarations… All declarations are type-correct.
stderr:
parsed in 0.000428s, checked in 0.000050s
Test "tutorial/007_betaReduction2"
Expected: 👍 accept · Size: 1.4 KB · Lines: 28 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Lambda reduction under binder
Test result: 👍 accepted · exit code 0 · wall time: 6 ms · instructions: 12.7 M · max rss memory: 5.9 MB
stdout:
Checking 2 declarations… All declarations are type-correct.
stderr:
parsed in 0.000567s, checked in 0.000051s
Test "tutorial/008_forallSortWhnf"
Expected: 👍 accept · Size: 1.2 KB · Lines: 25 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
The binding domain of a forall may need to be reduce before it is a sort
Test result: 👍 accepted · exit code 0 · wall time: 6 ms · instructions: 12.7 M · max rss memory: 5.9 MB
stdout:
Checking 2 declarations… All declarations are type-correct.
stderr:
parsed in 0.000469s, checked in 0.000050s
Test "tutorial/009_forallSortBad"
Expected: ✋ reject · Size: 1.2 KB · Lines: 26 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
The binding domain of a forall has to be a sort
Test result: ✋ rejected · exit code 1 · wall time: 271 ms · instructions: 13.2 M · max rss memory: 6.0 MB
stderr:
Unexpected error during type checking RPython traceback: File "implement.c", line 25, in main File "rpylean__rcli.c", line 121, in CLI_main File "rpylean_cli.c", line 1405, in check File "rpython_flowspace.c", line 812, in GeneratorIterator_next File "rpylean_environment.c", line 3887, in Environment__check_one File "rpylean_objects.c", line 33826, in W_Declaration_type_check File "rpylean_objects.c", line 49022, in DefOrTheorem_type_check File "rpylean_objects.c", line 29145, in W_ForAll_infer File "rpylean_environment.c", line 3538, in Environment_infer_sort_of File "rpylean_objects.c", line 29145, in W_ForAll_infer File "rpylean_environment.c", line 3538, in Environment_infer_sort_of File "rpylean_objects.c", line 28995, in W_ForAll_infer File "rpylean_environment.c", line 3698, in Environment_infer_sort_of Fatal RPython error: RuntimeError
Test "tutorial/010_nonTypeType"
Expected: ✋ reject · Size: 1.1 KB · Lines: 21 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
The type of a declaration has to be a type, not some other expression
Test result: ✋ rejected · exit code 1 · wall time: 11 ms · instructions: 12.6 M · max rss memory: 5.8 MB
stdout:
Checking 2 declarations…
stderr:
in nonTypeType: constType has type Type → Type → Type but is expected to be a Sort (Type or Prop) parsed in 0.000801s, checked in 0.000116s
Test "tutorial/011_nonPropThm"
Expected: ✋ reject · Size: 428 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
The type of a theorem has to be a proposition
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 12.6 M · max rss memory: 5.8 MB
stdout:
Checking 1 declaration… All declarations are type-correct.
stderr:
parsed in 0.000745s, checked in 0.000052s
Test "tutorial/012_levelComp1"
Expected: 👍 accept · Size: 395 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Some level computation
Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 12.4 M · max rss memory: 5.8 MB
stdout:
Checking 1 declaration… All declarations are type-correct.
stderr:
parsed in 0.000647s, checked in 0.000057s
Test "tutorial/013_levelComp2"
Expected: 👍 accept · Size: 413 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Some level computation
Test result: 👍 accepted · exit code 0 · wall time: 22 ms · instructions: 12.4 M · max rss memory: 5.8 MB
stdout:
Checking 1 declaration… All declarations are type-correct.
stderr:
parsed in 0.000517s, checked in 0.000057s
Test "tutorial/014_levelComp3"
Expected: 👍 accept · Size: 431 B · Lines: 9 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Some level computation
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 12.4 M · max rss memory: 5.8 MB
stdout:
Checking 1 declaration… All declarations are type-correct.
stderr:
parsed in 0.000503s, checked in 0.000055s
Test "tutorial/015_levelParams"
Expected: 👍 accept · Size: 1.4 KB · Lines: 29 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Level parameters
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 12.8 M · max rss memory: 5.9 MB
stdout:
Checking 2 declarations… All declarations are type-correct.
stderr:
parsed in 0.000632s, checked in 0.000082s
Test "tutorial/016_tut06_bad01"
Expected: ✋ reject · Size: 431 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Duplicate universe parameters
Test result: ✋ rejected · exit code 1 · wall time: 107 ms · instructions: 12.8 M · max rss memory: 5.8 MB
stderr:
RPython traceback: File "implement.c", line 25, in main File "rpylean__rcli.c", line 121, in CLI_main File "rpylean_cli.c", line 285, in check File "rpylean_cli.c", line 2685, in environment_from File "rpylean_environment.c", line 4677, in having Fatal RPython error: DuplicateLevels
Test "tutorial/017_levelComp4"
Expected: 👍 accept · Size: 428 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Some level computation
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 12.4 M · max rss memory: 5.8 MB
stdout:
Checking 1 declaration… All declarations are type-correct.
stderr:
parsed in 0.000600s, checked in 0.000042s
Test "tutorial/018_levelComp5"
Expected: 👍 accept · Size: 428 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Some level computation
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 12.4 M · max rss memory: 5.8 MB
stdout:
Checking 1 declaration… All declarations are type-correct.
stderr:
parsed in 0.000594s, checked in 0.000043s
Test "tutorial/019_imax1"
Expected: 👍 accept · Size: 813 B · Lines: 16 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Type inference for forall using imax
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 12.6 M · max rss memory: 5.8 MB
stdout:
Checking 1 declaration… All declarations are type-correct.
stderr:
parsed in 0.000649s, checked in 0.000070s
Test "tutorial/020_imax2"
Expected: 👍 accept · Size: 832 B · Lines: 17 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Type inference for forall using imax
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 12.5 M · max rss memory: 5.8 MB
stdout:
Checking 1 declaration… All declarations are type-correct.
stderr:
parsed in 0.000725s, checked in 0.000069s
Test "tutorial/021_inferVar"
Expected: 👍 accept · Size: 717 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Type inference of local variables
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 12.6 M · max rss memory: 5.8 MB
stdout:
Checking 1 declaration… All declarations are type-correct.
stderr:
parsed in 0.000666s, checked in 0.000081s
Test "tutorial/022_defEqLambda"
Expected: 👍 accept · Size: 1.4 KB · Lines: 26 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Definitional equality between lambdas
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 12.8 M · max rss memory: 5.9 MB
stdout:
Checking 1 declaration… All declarations are type-correct.
stderr:
parsed in 0.000721s, checked in 0.000117s
Test "tutorial/023_peano1"
Expected: 👍 accept · Size: 3.6 KB · Lines: 73 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Peano arithmetic: 2 = 2
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 13.8 M · max rss memory: 6.1 MB
stdout:
Checking 7 declarations… All declarations are type-correct.
stderr:
parsed in 0.001064s, checked in 0.000348s
Test "tutorial/024_peano2"
Expected: 👍 accept · Size: 4.5 KB · Lines: 90 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Peano arithmetic: 1 + 1 = 2
Test result: 👍 accepted · exit code 0 · wall time: 10 ms · instructions: 14.2 M · max rss memory: 6.1 MB
stdout:
Checking 8 declarations… All declarations are type-correct.
stderr:
parsed in 0.000638s, checked in 0.000198s
Test "tutorial/025_peano3"
Expected: 👍 accept · Size: 4.9 KB · Lines: 98 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Peano arithmetic: 2 * 2 = 4
Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 14.5 M · max rss memory: 6.2 MB
stdout:
Checking 10 declarations… All declarations are type-correct.
stderr:
parsed in 0.001265s, checked in 0.000599s
Test "tutorial/026_letType"
Expected: 👍 accept · Size: 493 B · Lines: 9 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Type checking a non-dependent let
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 12.5 M · max rss memory: 5.8 MB
stdout:
Checking 1 declaration… All declarations are type-correct.
stderr:
parsed in 0.000687s, checked in 0.000057s
Test "tutorial/027_letTypeDep"
Expected: 👍 accept · Size: 1.2 KB · Lines: 26 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Type checking a dependent let
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 12.7 M · max rss memory: 5.8 MB
stdout:
Checking 3 declarations… All declarations are type-correct.
stderr:
parsed in 0.000722s, checked in 0.000062s
Test "tutorial/028_letRed"
Expected: 👍 accept · Size: 631 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Reducing a let
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 12.5 M · max rss memory: 5.8 MB
stdout:
Checking 2 declarations… All declarations are type-correct.
stderr:
parsed in 0.000627s, checked in 0.000072s
Test "tutorial/029_empty"
Expected: 👍 accept · Size: 1.2 KB · Lines: 20 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A simple empty inductive type
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 12.6 M · max rss memory: 5.8 MB
stdout:
Checking 3 declarations… All declarations are type-correct.
stderr:
parsed in 0.000716s, checked in 0.000038s
Test "tutorial/030_boolType"
Expected: 👍 accept · Size: 2.3 KB · Lines: 37 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A simple enumeration inductive type
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 12.9 M · max rss memory: 5.9 MB
stdout:
Checking 5 declarations… All declarations are type-correct.
stderr:
parsed in 0.000801s, checked in 0.000055s
Test "tutorial/031_twoBool"
Expected: 👍 accept · Size: 4.2 KB · Lines: 65 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A simple product type
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 13.3 M · max rss memory: 5.9 MB
stdout:
Checking 8 declarations… All declarations are type-correct.
stderr:
parsed in 0.001055s, checked in 0.000037s
Test "tutorial/032_andType"
Expected: 👍 accept · Size: 3.2 KB · Lines: 57 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A parametrized product type (no level parameters)
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 13.2 M · max rss memory: 5.9 MB
stdout:
Checking 4 declarations… All declarations are type-correct.
stderr:
parsed in 0.000907s, checked in 0.000061s
Test "tutorial/033_prodType"
Expected: 👍 accept · Size: 3.8 KB · Lines: 76 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A parametrized product type (with level parameters)
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 13.3 M · max rss memory: 5.9 MB
stdout:
Checking 4 declarations… All declarations are type-correct.
stderr:
parsed in 0.000958s, checked in 0.000064s
Test "tutorial/034_pprodType"
Expected: 👍 accept · Size: 3.8 KB · Lines: 75 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A parametrized product type (with more general level parameters)
Test result: 👍 accepted · exit code 0 · wall time: 8 ms · instructions: 13.3 M · max rss memory: 5.9 MB
stdout:
Checking 4 declarations… All declarations are type-correct.
stderr:
parsed in 0.000583s, checked in 0.000034s
Test "tutorial/035_pUnitType"
Expected: 👍 accept · Size: 1.8 KB · Lines: 31 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Level-polymorphic unit type
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 12.8 M · max rss memory: 5.9 MB
stdout:
Checking 4 declarations… All declarations are type-correct.
stderr:
parsed in 0.000864s, checked in 0.000044s
Test "tutorial/036_eqType"
Expected: 👍 accept · Size: 3.2 KB · Lines: 62 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Equality, as an important indexed non-recursive data type
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 13.3 M · max rss memory: 5.9 MB
stdout:
Checking 4 declarations… All declarations are type-correct.
stderr:
parsed in 0.000891s, checked in 0.000076s
Test "tutorial/037_natDef"
Expected: 👍 accept · Size: 3.3 KB · Lines: 61 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A recursive inductive data type
Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 13.1 M · max rss memory: 5.9 MB
stdout:
Checking 5 declarations… All declarations are type-correct.
stderr:
parsed in 0.000830s, checked in 0.000043s
Test "tutorial/038_rbTreeDef"
Expected: 👍 accept · Size: 15.7 KB · Lines: 296 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A recursive indexed data type
Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 16.1 M · max rss memory: 6.4 MB
stdout:
Checking 14 declarations… All declarations are type-correct.
stderr:
parsed in 0.002169s, checked in 0.000079s
Test "tutorial/039_inductBadNonSort"
Expected: ✋ reject · Size: 1.2 KB · Lines: 20 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
An inductive type with a non-sort type
Test result: ✋ rejected · exit code 1 · wall time: 11 ms · instructions: 12.7 M · max rss memory: 5.8 MB
stdout:
Checking 2 declarations…
stderr:
in inductBadNonSort: constType has type Type → Type → Type but is expected to be a Sort (Type or Prop) parsed in 0.000751s, checked in 0.000133s
Test "tutorial/040_inductBadNonSort2"
Expected: ✋ reject · Size: 602 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Another inductive type with a non-sort type
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 12.4 M · max rss memory: 5.8 MB
stdout:
Checking 2 declarations… All declarations are type-correct.
stderr:
parsed in 0.000675s, checked in 0.000028s
Test "tutorial/041_inductLevelParam"
Expected: ✋ reject · Size: 519 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
An inductive with duplicate level params
Test result: ✋ rejected · exit code 1 · wall time: 105 ms · instructions: 12.8 M · max rss memory: 5.8 MB
stderr:
RPython traceback: File "implement.c", line 25, in main File "rpylean__rcli.c", line 121, in CLI_main File "rpylean_cli.c", line 285, in check File "rpylean_cli.c", line 2685, in environment_from File "rpylean_environment.c", line 4677, in having Fatal RPython error: DuplicateLevels
Test "tutorial/042_inductTooFewParams"
Expected: ✋ reject · Size: 552 B · Lines: 6 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
An inductive with too few parameters in the type
Test result: 👍 accepted · exit code 0 · wall time: 8 ms · instructions: 12.5 M · max rss memory: 5.8 MB
stdout:
Checking 1 declaration… All declarations are type-correct.
stderr:
parsed in 0.000413s, checked in 0.000017s
Test "tutorial/043_inductWrongCtorParams"
Expected: ✋ reject · Size: 1.2 KB · Lines: 16 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
An inductive with a constructor with wrong parameters
Test result: 👍 accepted · exit code 0 · wall time: 8 ms · instructions: 12.6 M · max rss memory: 5.8 MB
stdout:
Checking 4 declarations… All declarations are type-correct.
stderr:
parsed in 0.000337s, checked in 0.000017s
Test "tutorial/044_inductWrongCtorResParams"
Expected: ✋ reject · Size: 1.3 KB · Lines: 19 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
An inductive with a constructor with wrong parameters in result (they are swapped)
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 12.7 M · max rss memory: 5.8 MB
stdout:
Checking 3 declarations… All declarations are type-correct.
stderr:
parsed in 0.000674s, checked in 0.000029s
Test "tutorial/045_inductWrongCtorResLevel"
Expected: ✋ reject · Size: 1.4 KB · Lines: 23 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
An inductive with a constructor with wrong level parameters in result (they are swapped)
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 12.7 M · max rss memory: 5.8 MB
stdout:
Checking 3 declarations… All declarations are type-correct.
stderr:
parsed in 0.000756s, checked in 0.000031s
Test "tutorial/046_inductInIndex"
Expected: ✋ reject · Size: 1.1 KB · Lines: 14 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A constructor with an unexpected occurrence of the type in index position of a return type.
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 12.5 M · max rss memory: 5.8 MB
stdout:
Checking 4 declarations… All declarations are type-correct.
stderr:
parsed in 0.000709s, checked in 0.000034s
Test "tutorial/047_indNeg"
Expected: ✋ reject · Size: 1000 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
The classic example of an inductive with negative recursive occurrence
Test result: 👍 accepted · exit code 0 · wall time: 8 ms · instructions: 12.5 M · max rss memory: 5.8 MB
stdout:
Checking 3 declarations… All declarations are type-correct.
stderr:
parsed in 0.000504s, checked in 0.000025s
Test "tutorial/048_reduceCtorParam.mk"
Expected: 👍 accept · Size: 4.1 KB · Lines: 80 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
When checking inductives, we expect the kernel to reduce the types of constructor arguments.
Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 13.4 M · max rss memory: 6.0 MB
stdout:
Checking 5 declarations… All declarations are type-correct.
stderr:
parsed in 0.000778s, checked in 0.000067s
Test "tutorial/049_reduceCtorType.mk"
Expected: ✋ reject · Size: 1.5 KB · Lines: 26 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
When checking inductives, we expect the kernel to not reduce the type of the constructor itself;
that should be all manifest foralls
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 12.7 M · max rss memory: 5.9 MB
stdout:
Checking 4 declarations… All declarations are type-correct.
stderr:
parsed in 0.000779s, checked in 0.000150s
Test "tutorial/050_indNegReducible"
Expected: ✋ reject · Size: 1.9 KB · Lines: 31 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
When checking inductives, we expect the kernel to not reduce the type of the constructor parameters further than head normal form. Recursive occurrences nested inside the head normal form are considered negative occurrences, even if they could be reduced to disappear.
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 12.8 M · max rss memory: 5.9 MB
stdout:
Checking 5 declarations… All declarations are type-correct.
stderr:
parsed in 0.000704s, checked in 0.000081s
Test "tutorial/051_predWithTypeField"
Expected: 👍 accept · Size: 2.0 KB · Lines: 32 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
An inductive proposition can have constructors with fields of arbitrary level.
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 12.8 M · max rss memory: 5.9 MB
stdout:
Checking 4 declarations… All declarations are type-correct.
stderr:
parsed in 0.000818s, checked in 0.000058s
Test "tutorial/052_typeWithTypeField"
Expected: 👍 accept · Size: 2.1 KB · Lines: 36 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
An inductive type can have fields of level up to that of the inductive.
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 12.8 M · max rss memory: 5.9 MB
stdout:
Checking 4 declarations… All declarations are type-correct.
stderr:
parsed in 0.000843s, checked in 0.000040s
Test "tutorial/053_typeWithTypeFieldPoly"
Expected: 👍 accept · Size: 2.1 KB · Lines: 38 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
An inductive type can have fields of level up to that of the inductive (polymorphic variant).
Test result: 👍 accepted · exit code 0 · wall time: 8 ms · instructions: 12.8 M · max rss memory: 5.9 MB
stdout:
Checking 4 declarations… All declarations are type-correct.
stderr:
parsed in 0.000599s, checked in 0.000025s
Test "tutorial/054_typeWithTooHighTypeField.mk"
Expected: ✋ reject · Size: 947 B · Lines: 11 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
An inductive type can have fields of from higher universes.
Test result: 👍 accepted · exit code 0 · wall time: 14 ms · instructions: 12.6 M · max rss memory: 5.8 MB
stdout:
Checking 3 declarations… All declarations are type-correct.
stderr:
parsed in 0.000747s, checked in 0.000028s
Test "tutorial/055_emptyRec"
Expected: 👍 accept · Size: 1.2 KB · Lines: 21 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of the generated recursor
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 12.7 M · max rss memory: 5.9 MB
stdout:
Checking 3 declarations… All declarations are type-correct.
stderr:
parsed in 0.000830s, checked in 0.000093s
Test "tutorial/056_boolRec"
Expected: 👍 accept · Size: 3.0 KB · Lines: 53 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of the generated recursor
Test result: 👍 accepted · exit code 0 · wall time: 10 ms · instructions: 13.2 M · max rss memory: 5.9 MB
stdout:
Checking 5 declarations… All declarations are type-correct.
stderr:
parsed in 0.000921s, checked in 0.000129s
Test "tutorial/057_twoBoolRec"
Expected: 👍 accept · Size: 4.8 KB · Lines: 78 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of the generated recursor
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 13.6 M · max rss memory: 6.0 MB
stdout:
Checking 8 declarations… All declarations are type-correct.
stderr:
parsed in 0.001093s, checked in 0.000135s
Test "tutorial/058_andRec"
Expected: 👍 accept · Size: 3.2 KB · Lines: 58 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of the generated recursor
Test result: 👍 accepted · exit code 0 · wall time: 21 ms · instructions: 13.3 M · max rss memory: 6.0 MB
stdout:
Checking 4 declarations… All declarations are type-correct.
stderr:
parsed in 0.000937s, checked in 0.000165s
Test "tutorial/059_prodRec"
Expected: 👍 accept · Size: 4.0 KB · Lines: 79 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of the generated recursor
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 13.5 M · max rss memory: 6.0 MB
stdout:
Checking 4 declarations… All declarations are type-correct.
stderr:
parsed in 0.001056s, checked in 0.000200s
Test "tutorial/060_pprodRec"
Expected: 👍 accept · Size: 4.0 KB · Lines: 78 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of the generated recursor
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 13.5 M · max rss memory: 6.0 MB
stdout:
Checking 4 declarations… All declarations are type-correct.
stderr:
parsed in 0.001070s, checked in 0.000171s
Test "tutorial/061_punitRec"
Expected: 👍 accept · Size: 2.2 KB · Lines: 39 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of the generated recursor
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 12.9 M · max rss memory: 5.9 MB
stdout:
Checking 4 declarations… All declarations are type-correct.
stderr:
parsed in 0.000882s, checked in 0.000101s
Test "tutorial/062_eqRec"
Expected: 👍 accept · Size: 3.3 KB · Lines: 63 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of the generated recursor
Test result: 👍 accepted · exit code 0 · wall time: 8 ms · instructions: 13.3 M · max rss memory: 6.0 MB
stdout:
Checking 4 declarations… All declarations are type-correct.
stderr:
parsed in 0.000698s, checked in 0.000085s
Test "tutorial/063_nRec"
Expected: 👍 accept · Size: 3.3 KB · Lines: 61 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of the generated recursor
Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 13.3 M · max rss memory: 5.9 MB
stdout:
Checking 5 declarations… All declarations are type-correct.
stderr:
parsed in 0.001050s, checked in 0.000128s
Test "tutorial/064_rbTreeRef"
Expected: 👍 accept · Size: 16.2 KB · Lines: 303 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of the generated recursor
Test result: 👍 accepted · exit code 0 · wall time: 14 ms · instructions: 17.0 M · max rss memory: 6.8 MB
stdout:
Checking 14 declarations… All declarations are type-correct.
stderr:
parsed in 0.002230s, checked in 0.000608s
Test "tutorial/065_boolPropRec"
Expected: 👍 accept · Size: 2.3 KB · Lines: 34 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Inductive predicates eliminate into Prop if they have more than one constructor.
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 12.9 M · max rss memory: 5.9 MB
stdout:
Checking 5 declarations… All declarations are type-correct.
stderr:
parsed in 0.000846s, checked in 0.000112s
Test "tutorial/066_existsRec"
Expected: 👍 accept · Size: 3.6 KB · Lines: 66 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Inductive predicates eliminate into Prop if they have one constructors and it carries data.
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 13.5 M · max rss memory: 6.0 MB
stdout:
Checking 4 declarations… All declarations are type-correct.
stderr:
parsed in 0.000917s, checked in 0.000246s
Test "tutorial/067_sortElimPropRec"
Expected: 👍 accept · Size: 5.6 KB · Lines: 97 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Inductive predicates eliminate into Sort if they have one constructors and it carries data, but the data is known from the type, e.g. a parameter or an index
Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 13.9 M · max rss memory: 6.0 MB
stdout:
Checking 8 declarations… All declarations are type-correct.
stderr:
parsed in 0.001173s, checked in 0.000208s
Test "tutorial/068_sortElimProp2Rec"
Expected: 👍 accept · Size: 6.6 KB · Lines: 114 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Inductive predicates eliminate into Sort if they have one constructors and it carries data, but the data is known from the type, e.g. a parameter or an index. However, it must occur directly in the result type, with no intervening reduction.
Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 14.2 M · max rss memory: 6.1 MB
stdout:
Checking 9 declarations… All declarations are type-correct.
stderr:
parsed in 0.001319s, checked in 0.000222s
Test "tutorial/069_boolRecEqns"
Expected: 👍 accept · Size: 10.8 KB · Lines: 199 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Reduction behavior of Bool.rec
Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 15.1 M · max rss memory: 6.2 MB
stdout:
Checking 11 declarations… All declarations are type-correct.
stderr:
parsed in 0.001603s, checked in 0.000160s
Test "tutorial/070_prodRecEqns"
Expected: 👍 accept · Size: 10.1 KB · Lines: 205 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Reduction behavior of Prod.rec
Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 15.5 M · max rss memory: 6.4 MB
stdout:
Checking 7 declarations… All declarations are type-correct.
stderr:
parsed in 0.001750s, checked in 0.000502s
Test "tutorial/071_nRecReduction"
Expected: 👍 accept · Size: 12.7 KB · Lines: 238 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A proof relying on the reduction behavior of N.rec
Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 16.0 M · max rss memory: 6.5 MB
stdout:
Checking 13 declarations… All declarations are type-correct.
stderr:
parsed in 0.001820s, checked in 0.000407s
Test "tutorial/072_listRecReduction"
Expected: 👍 accept · Size: 17.5 KB · Lines: 335 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Reduction behavior of List.rec
Test result: 👍 accepted · exit code 0 · wall time: 14 ms · instructions: 18.2 M · max rss memory: 7.0 MB
stdout:
Checking 14 declarations… All declarations are type-correct.
stderr:
parsed in 0.002371s, checked in 0.001031s
Test "tutorial/073_RBTree.id_spec"
Expected: 👍 accept · Size: 47.9 KB · Lines: 1.0 k · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Reduction behavior of RBTree.rec
Test result: 👍 accepted · exit code 0 · wall time: 19 ms · instructions: 25.6 M · max rss memory: 8.4 MB
stdout:
Checking 19 declarations… All declarations are type-correct.
stderr:
parsed in 0.005310s, checked in 0.000946s
Test "tutorial/074_And.right"
Expected: 👍 accept · Size: 4.3 KB · Lines: 74 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Type-checking simple projection functions
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 13.5 M · max rss memory: 6.0 MB
stdout:
Checking 5 declarations… All declarations are type-correct.
stderr:
parsed in 0.001068s, checked in 0.000157s
Test "tutorial/075_Prod.snd"
Expected: 👍 accept · Size: 4.5 KB · Lines: 83 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Type-checking projection functions with parameters
Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 13.7 M · max rss memory: 6.0 MB
stdout:
Checking 5 declarations… All declarations are type-correct.
stderr:
parsed in 0.001107s, checked in 0.000170s
Test "tutorial/076_PProd.snd"
Expected: 👍 accept · Size: 4.5 KB · Lines: 83 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Type-checking projection functions
Test result: 👍 accepted · exit code 0 · wall time: 8 ms · instructions: 13.6 M · max rss memory: 6.0 MB
stdout:
Checking 5 declarations… All declarations are type-correct.
stderr:
parsed in 0.000556s, checked in 0.000075s
Test "tutorial/077_PSigma.snd"
Expected: 👍 accept · Size: 5.1 KB · Lines: 96 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Type-checking dependent projection functions
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 13.8 M · max rss memory: 6.0 MB
stdout:
Checking 5 declarations… All declarations are type-correct.
stderr:
parsed in 0.000714s, checked in 0.000102s
Test "tutorial/078_projOutOfRange"
Expected: ✋ reject · Size: 3.8 KB · Lines: 67 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Out of range projection
Test result: ✋ rejected · exit code 1 · wall time: 101 ms · instructions: 13.6 M · max rss memory: 6.0 MB
stderr:
Unexpected error during type checking RPython traceback: File "implement.c", line 25, in main File "rpylean__rcli.c", line 121, in CLI_main ... Fatal RPython error: RuntimeError
Test "tutorial/079_projNotStruct"
Expected: ✋ reject · Size: 3.5 KB · Lines: 64 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Projection out something that is not a structure
Test result: ✋ rejected · exit code 1 · wall time: 119 ms · instructions: 13.5 M · max rss memory: 6.0 MB
stderr:
RPython traceback: File "rpylean_environment.c", line 3887, in Environment__check_one File "rpylean_objects.c", line 33826, in W_Declaration_type_check File "rpylean_objects.c", line 49022, in DefOrTheorem_type_check File "rpylean_objects.c", line 34813, in W_Lambda_infer File "rpylean_objects.c", line 4016, in W_Proj_infer Fatal RPython error: AssertionError
Test "tutorial/080_projProp1"
Expected: 👍 accept · Size: 8.2 KB · Lines: 143 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Projecting out of a proposition
The lean kernel allows projections out of propositions if they precede all dependent data fields.
Test result: 👍 accepted · exit code 0 · wall time: 8 ms · instructions: 14.3 M · max rss memory: 6.1 MB
stdout:
Checking 10 declarations… All declarations are type-correct.
stderr:
parsed in 0.000888s, checked in 0.000044s
Test "tutorial/081_projProp2"
Expected: ✋ reject · Size: 8.2 KB · Lines: 143 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Projecting out of a proposition
The lean kernel disallows data projections out of propositional structures.
Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 14.3 M · max rss memory: 6.1 MB
stdout:
Checking 10 declarations… All declarations are type-correct.
stderr:
parsed in 0.001331s, checked in 0.000087s
Test "tutorial/082_projProp3"
Expected: 👍 accept · Size: 8.2 KB · Lines: 143 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Projecting out of a proposition
The lean kernel allows projections out of propositions if they precede all dependent data fields. Non-dependent data fields are not relevant.
Test result: 👍 accepted · exit code 0 · wall time: 14 ms · instructions: 14.3 M · max rss memory: 6.1 MB
stdout:
Checking 10 declarations… All declarations are type-correct.
stderr:
parsed in 0.001579s, checked in 0.000089s
Test "tutorial/083_projProp4"
Expected: ✋ reject · Size: 8.2 KB · Lines: 143 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Projecting out of a proposition
The lean kernel disallows data projections out of propositional structures.
Test result: 👍 accepted · exit code 0 · wall time: 14 ms · instructions: 14.3 M · max rss memory: 6.1 MB
stdout:
Checking 10 declarations… All declarations are type-correct.
stderr:
parsed in 0.001589s, checked in 0.000096s
Test "tutorial/084_projProp5"
Expected: ✋ reject · Size: 8.4 KB · Lines: 148 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Projecting out of a proposition
The lean kernel disallows proof projections out of propositional structures that depend on data.
Test result: 👍 accepted · exit code 0 · wall time: 14 ms · instructions: 14.4 M · max rss memory: 6.1 MB
stdout:
Checking 10 declarations… All declarations are type-correct.
stderr:
parsed in 0.001675s, checked in 0.000119s
Test "tutorial/085_projProp6"
Expected: ✋ reject · Size: 8.2 KB · Lines: 143 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Projecting out of a proposition.
The lean kernel rejects any projections out of a proposition that come after a dependent data field, even if that is not used by the present projection.
Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 14.3 M · max rss memory: 6.1 MB
stdout:
Checking 10 declarations… All declarations are type-correct.
stderr:
parsed in 0.001490s, checked in 0.000113s
Test "tutorial/086_projDataIndexRec"
Expected: 👍 accept · Size: 6.8 KB · Lines: 111 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
The recursor for ProjDataIndex allows elimination into sort.
Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 14.0 M · max rss memory: 6.0 MB
stdout:
Checking 11 declarations… All declarations are type-correct.
stderr:
parsed in 0.001262s, checked in 0.000133s
Test "tutorial/087_projIndexData"
Expected: ✋ reject · Size: 6.8 KB · Lines: 111 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Projecting out data is not allowed, even if this data appears as an index and the recursor would allow it.
Test result: ✋ rejected · exit code 1 · wall time: 125 ms · instructions: 14.3 M · max rss memory: 6.1 MB
stderr:
Unexpected error during type checking RPython traceback: File "implement.c", line 25, in main File "rpylean__rcli.c", line 121, in CLI_main ... Fatal RPython error: RuntimeError
Test "tutorial/088_projIndexData2"
Expected: ✋ reject · Size: 6.8 KB · Lines: 111 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Projecting out data is not allowed, even if this data appears as an index and the recursor would allow it.
This also forbids projecting out proofs that follow such fields.
Test result: ✋ rejected · exit code 1 · wall time: 130 ms · instructions: 14.3 M · max rss memory: 6.1 MB
stderr:
Unexpected error during type checking RPython traceback: File "implement.c", line 25, in main File "rpylean__rcli.c", line 121, in CLI_main ... Fatal RPython error: RuntimeError
Test "tutorial/089_projRed"
Expected: 👍 accept · Size: 9.9 KB · Lines: 177 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Projection reductions
Test result: 👍 accepted · exit code 0 · wall time: 8 ms · instructions: 14.9 M · max rss memory: 6.2 MB
stdout:
Checking 13 declarations… All declarations are type-correct.
stderr:
parsed in 0.001049s, checked in 0.000096s
Test "tutorial/090_ruleK"
Expected: 👍 accept · Size: 6.5 KB · Lines: 121 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Rule k for Eq:
The recursor reduces even if the major argument is not a constructor,
as long replacing the major argument with a constructor is type correct.
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 14.1 M · max rss memory: 6.1 MB
stdout:
Checking 8 declarations… All declarations are type-correct.
stderr:
parsed in 0.001216s, checked in 0.000197s
Test "tutorial/091_ruleKbad"
Expected: ✋ reject · Size: 6.5 KB · Lines: 121 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Rule k for Eq should not fire if the types of the major argument
do not match that of the constructor.
Test result: ✋ rejected · exit code 1 · wall time: 12 ms · instructions: 14.2 M · max rss memory: 6.1 MB
stdout:
Checking 8 declarations…
stderr:
in ruleKbad:
fun x.«_@».Tutorial.3161876795._hygCtx._hyg.27 a ↦ Eq.refl.{1} Bool a
has type
Eq.{1} Bool Bool.true Bool.false → (a : Bool) → Eq.{1} Bool a a
but is expected to have type
(h : Eq.{1} Bool Bool.true Bool.false) → (a : Bool) → Eq.{1} Bool (Eq.rec.{1, 1} Bool Bool.true (fun x.«_@».Tutorial.3161876795._hygCtx._hyg.17 x.«_@».Tutorial.3161876795._hygCtx._hyg.19 ↦ Bool) a Bool.false h) a
parsed in 0.001211s, checked in 0.000306s
Test "tutorial/092_ruleKAcc"
Expected: ✋ reject · Size: 12.8 KB · Lines: 238 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Rule k should not fire for Acc.
Test result: ✋ rejected · exit code 1 · wall time: 12 ms · instructions: 15.9 M · max rss memory: 6.5 MB
stdout:
Checking 11 declarations…
stderr:
in ruleKAcc:
fun α p x h a ↦ Eq.refl.{1} Bool a
has type
(α : Sort u) → (p : α → ∀ (a.«_@»._internal._hyg.0 : α), Prop) → (x : α) → Acc.{u} α p x → (a : Bool) → Eq.{1} Bool a a
but is expected to have type
(α : Sort u) → (p : α → ∀ (a.«_@»._internal._hyg.0 : α), Prop) → (x : α) → (h : Acc.{u} α p x) → (a : Bool) → Eq.{1} Bool (Acc.rec.{1, u} α p (fun x.«_@».Tutorial.4255978773._hygCtx._hyg.22 x.«_@».Tutorial.4255978773._hygCtx._hyg.24 ↦ Bool) (fun x.«_@».Tutorial.4255978773._hygCtx._hyg.31 x.«_@».Tutorial.4255978773._hygCtx._hyg.33 x.«_@».Tutorial.4255978773._hygCtx._hyg.35 ↦ a) x h) a
parsed in 0.001808s, checked in 0.000481s
Test "tutorial/093_aNatLit"
Expected: 👍 accept · Size: 3.0 KB · Lines: 54 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Type checking Nat literals
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 13.1 M · max rss memory: 5.9 MB
stdout:
Checking 5 declarations… All declarations are type-correct.
stderr:
parsed in 0.000922s, checked in 0.000051s
Test "tutorial/094_natLitEq"
Expected: 👍 accept · Size: 6.1 KB · Lines: 114 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Reducing Nat literals
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 13.9 M · max rss memory: 6.0 MB
stdout:
Checking 8 declarations… All declarations are type-correct.
stderr:
parsed in 0.001332s, checked in 0.000105s
Test "tutorial/095_proofIrrelevance"
Expected: 👍 accept · Size: 5.0 KB · Lines: 100 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Proof irrelevance
Test result: ✋ rejected · exit code 1 · wall time: 22 ms · instructions: 13.8 M · max rss memory: 6.0 MB
stdout:
Checking 5 declarations…
stderr:
in proofIrrelevance:
fun x.«_@».Tutorial.3753928780._hygCtx._hyg.15 x.«_@».Tutorial.3753928780._hygCtx._hyg.17 x.«_@».Tutorial.3753928780._hygCtx._hyg.19 ↦ rfl.{0} x.«_@».Tutorial.3753928780._hygCtx._hyg.15 x.«_@».Tutorial.3753928780._hygCtx._hyg.17
has type
(x.«_@».Tutorial.3753928780._hygCtx._hyg.15 : Prop) → (x.«_@».Tutorial.3753928780._hygCtx._hyg.17 : x.«_@».Tutorial.3753928780._hygCtx._hyg.15) → x.«_@».Tutorial.3753928780._hygCtx._hyg.15 → Eq.{0} x.«_@».Tutorial.3753928780._hygCtx._hyg.15 x.«_@».Tutorial.3753928780._hygCtx._hyg.17 x.«_@».Tutorial.3753928780._hygCtx._hyg.17
but is expected to have type
(p : Prop) → (h1 : p) → (h2 : p) → Eq.{0} p h1 h2
parsed in 0.001066s, checked in 0.000249s
Test "tutorial/096_unitEta1"
Expected: 👍 accept · Size: 6.2 KB · Lines: 116 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Unit eta
Test result: ✋ rejected · exit code 1 · wall time: 11 ms · instructions: 14.1 M · max rss memory: 6.0 MB
stdout:
Checking 9 declarations…
stderr:
in unitEta1:
fun x.«_@».Tutorial.1036685737._hygCtx._hyg.14 x.«_@».Tutorial.1036685737._hygCtx._hyg.16 ↦ rfl.{1} Unit x.«_@».Tutorial.1036685737._hygCtx._hyg.14
has type
(x.«_@».Tutorial.1036685737._hygCtx._hyg.14 : Unit) → Unit → Eq.{1} Unit x.«_@».Tutorial.1036685737._hygCtx._hyg.14 x.«_@».Tutorial.1036685737._hygCtx._hyg.14
but is expected to have type
(x : Unit) → (y : Unit) → Eq.{1} Unit x y
parsed in 0.000771s, checked in 0.000101s
Test "tutorial/097_unitEta2"
Expected: 👍 accept · Size: 6.0 KB · Lines: 109 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Unit eta
Test result: ✋ rejected · exit code 1 · wall time: 11 ms · instructions: 14.0 M · max rss memory: 6.0 MB
stdout:
Checking 8 declarations…
stderr:
in unitEta2:
fun x.«_@».Tutorial.1006014971._hygCtx._hyg.14 x.«_@».Tutorial.1006014971._hygCtx._hyg.16 ↦ rfl.{u} PUnit.{u} x.«_@».Tutorial.1006014971._hygCtx._hyg.14
has type
(x.«_@».Tutorial.1006014971._hygCtx._hyg.14 : PUnit.{u}) → PUnit.{u} → Eq.{u} PUnit.{u} x.«_@».Tutorial.1006014971._hygCtx._hyg.14 x.«_@».Tutorial.1006014971._hygCtx._hyg.14
but is expected to have type
(x : PUnit.{u}) → (y : PUnit.{u}) → Eq.{u} PUnit.{u} x y
parsed in 0.001134s, checked in 0.000257s
Test "tutorial/098_unitEta3"
Expected: 👍 accept · Size: 6.0 KB · Lines: 111 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Unit eta
Test result: ✋ rejected · exit code 1 · wall time: 12 ms · instructions: 14.0 M · max rss memory: 6.1 MB
stdout:
Checking 8 declarations…
stderr:
in unitEta3:
fun x.«_@».Tutorial.1995346559._hygCtx._hyg.14 x.«_@».Tutorial.1995346559._hygCtx._hyg.16 ↦ rfl.{0} PUnit.{0} x.«_@».Tutorial.1995346559._hygCtx._hyg.14
has type
(x.«_@».Tutorial.1995346559._hygCtx._hyg.14 : PUnit.{0}) → PUnit.{0} → Eq.{0} PUnit.{0} x.«_@».Tutorial.1995346559._hygCtx._hyg.14 x.«_@».Tutorial.1995346559._hygCtx._hyg.14
but is expected to have type
(x : PUnit.{0}) → (y : PUnit.{0}) → Eq.{0} PUnit.{0} x y
parsed in 0.001253s, checked in 0.000210s
Test "tutorial/099_structEta"
Expected: 👍 accept · Size: 12.5 KB · Lines: 230 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Structure eta
Test result: 👍 accepted · exit code 0 · wall time: 13 ms · instructions: 16.0 M · max rss memory: 6.5 MB
stdout:
Checking 13 declarations… All declarations are type-correct.
stderr:
parsed in 0.001790s, checked in 0.000476s
Test "tutorial/100_funEta"
Expected: 👍 accept · Size: 5.2 KB · Lines: 104 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Function eta for non-dependent functions.
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 13.9 M · max rss memory: 6.0 MB
stdout:
Checking 5 declarations… All declarations are type-correct.
stderr:
parsed in 0.001117s, checked in 0.000204s
Test "tutorial/101_funEtaDep"
Expected: 👍 accept · Size: 5.3 KB · Lines: 106 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Function eta for dependent functions (pi types).
Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 13.9 M · max rss memory: 6.1 MB
stdout:
Checking 5 declarations… All declarations are type-correct.
stderr:
parsed in 0.001068s, checked in 0.000227s
Test "tutorial/102_funEtaBad"
Expected: ✋ reject · Size: 4.9 KB · Lines: 97 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Eta should not identify functions with different bodies.
Test result: ✋ rejected · exit code 1 · wall time: 11 ms · instructions: 13.9 M · max rss memory: 6.1 MB
stdout:
Checking 4 declarations…
stderr:
in funEtaBad:
fun x.«_@».Tutorial.4249243883._hygCtx._hyg.28 x.«_@».Tutorial.4249243883._hygCtx._hyg.30 x.«_@».Tutorial.4249243883._hygCtx._hyg.32 f ↦ Eq.refl.{1} (x.«_@».Tutorial.4249243883._hygCtx._hyg.28 → x.«_@».Tutorial.4249243883._hygCtx._hyg.30) f
has type
(x.«_@».Tutorial.4249243883._hygCtx._hyg.28 : Type) → (x.«_@».Tutorial.4249243883._hygCtx._hyg.30 : Type) → (x.«_@».Tutorial.4249243883._hygCtx._hyg.28 → x.«_@».Tutorial.4249243883._hygCtx._hyg.28) → (f : x.«_@».Tutorial.4249243883._hygCtx._hyg.28 → x.«_@».Tutorial.4249243883._hygCtx._hyg.30) → Eq.{1} (x.«_@».Tutorial.4249243883._hygCtx._hyg.28 → x.«_@».Tutorial.4249243883._hygCtx._hyg.30) f f
but is expected to have type
(α : Type) → (β : Type) → (g : α → α) → (f : α → β) → Eq.{1} (α → β) (fun x ↦ f (g x)) f
parsed in 0.001113s, checked in 0.000283s
Test "tutorial/103_etaRuleK"
Expected: ✋ reject · Size: 6.5 KB · Lines: 121 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Corner case for function eta: Does a defeq between a partially applied recursor with rule k and a free variable trigger eta expansion?
Taking the official kernel as the specification, the answer is no. See https://github.com/leanprover/lean4/issues/12520 for a discussion.
Test result: ✋ rejected · exit code 1 · wall time: 11 ms · instructions: 14.2 M · max rss memory: 6.1 MB
stdout:
Checking 8 declarations…
stderr:
in etaRuleK:
fun a ↦ Eq.refl.{1} (Eq.{1} Bool Bool.true Bool.true → Bool) a
has type
(a : Eq.{1} Bool Bool.true Bool.true → Bool) → Eq.{1} (Eq.{1} Bool Bool.true Bool.true → Bool) a a
but is expected to have type
(a : Eq.{1} Bool Bool.true Bool.true → Bool) → Eq.{1} (Eq.{1} Bool Bool.true Bool.true → Bool) (Eq.rec.{1, 1} Bool Bool.true (fun x.«_@».Tutorial.2477593770._hygCtx._hyg.31 x.«_@».Tutorial.2477593770._hygCtx._hyg.33 ↦ Bool) (a (Eq.refl.{1} Bool Bool.true)) Bool.true) a
parsed in 0.001158s, checked in 0.000283s
Test "tutorial/104_etaCtor"
Expected: ✋ reject · Size: 9.0 KB · Lines: 148 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Corner case for function eta: Does a defeq between a partially applied constructor trigger eta expansion?
Taking the official kernel as the specification, the answer is no. See https://github.com/leanprover/lean4/issues/12520 for a discussion.
Test result: ✋ rejected · exit code 1 · wall time: 12 ms · instructions: 14.5 M · max rss memory: 6.1 MB
stdout:
Checking 15 declarations…
stderr:
in etaCtor:
fun x ↦ Eq.refl.{1} (True → T) x
has type
(x : True → T) → Eq.{1} (True → T) x x
but is expected to have type
(x : True → T) → Eq.{1} (True → T) (T.mk (T.val (x True.intro))) x
parsed in 0.001416s, checked in 0.000185s
Test "tutorial/105_reflOccLeft"
Expected: ✋ reject · Size: 3.7 KB · Lines: 61 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Rejection: recursive occurrence on the left of an arrow, behind further arrows inside a constructor argument.
The constructor argument is a function type Nat → (I → Nat).
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 13.2 M · max rss memory: 5.9 MB
stdout:
Checking 7 declarations… All declarations are type-correct.
stderr:
parsed in 0.000987s, checked in 0.000032s
Test "tutorial/106_reflOccInIndex"
Expected: ✋ reject · Size: 4.0 KB · Lines: 66 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Rejection: recursive occurrence in index position, behind a further arrow.
We build an indexed inductive I : Type → Type with a constructor argument
Nat → I (I α), so the recursive occurrence appears as an index argument.
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 13.3 M · max rss memory: 5.9 MB
stdout:
Checking 7 declarations… All declarations are type-correct.
stderr:
parsed in 0.001015s, checked in 0.000029s
Test "tutorial/107_reduceCtorParamRefl.mk"
Expected: 👍 accept · Size: 4.5 KB · Lines: 88 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
When checking inductives, we expect the kernel to reduce the types of constructor arguments in all positive positions.
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 13.5 M · max rss memory: 6.0 MB
stdout:
Checking 5 declarations… All declarations are type-correct.
stderr:
parsed in 0.001044s, checked in 0.000079s
Test "tutorial/108_reduceCtorParamRefl2.mk"
Expected: 👍 accept · Size: 4.5 KB · Lines: 88 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
When checking inductives, we expect the kernel to reduce the types of constructor arguments in all positive positions.
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 13.5 M · max rss memory: 6.0 MB
stdout:
Checking 5 declarations… All declarations are type-correct.
stderr:
parsed in 0.001046s, checked in 0.000078s
Test "tutorial/109_rTreeRec"
Expected: 👍 accept · Size: 5.5 KB · Lines: 91 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of the generated recursor.
Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 13.8 M · max rss memory: 6.0 MB
stdout:
Checking 9 declarations… All declarations are type-correct.
stderr:
parsed in 0.001106s, checked in 0.000144s
Test "tutorial/110_rtreeRecReduction"
Expected: 👍 accept · Size: 10.8 KB · Lines: 193 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Reduction behavior of RTree.rec on RTree.mk.
Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 15.4 M · max rss memory: 6.4 MB
stdout:
Checking 14 declarations… All declarations are type-correct.
stderr:
parsed in 0.001677s, checked in 0.000379s
Test "tutorial/111_accRecType"
Expected: 👍 accept · Size: 7.5 KB · Lines: 151 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of Acc.rec.
Test result: 👍 accepted · exit code 0 · wall time: 8 ms · instructions: 14.6 M · max rss memory: 6.2 MB
stdout:
Checking 4 declarations… All declarations are type-correct.
stderr:
parsed in 0.000768s, checked in 0.000137s
Test "tutorial/112_accRecReduction"
Expected: 👍 accept · Size: 13.4 KB · Lines: 252 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Acc.rec reduces on Acc.intro.
Test result: 👍 accepted · exit code 0 · wall time: 13 ms · instructions: 16.6 M · max rss memory: 6.8 MB
stdout:
Checking 11 declarations… All declarations are type-correct.
stderr:
parsed in 0.001979s, checked in 0.000715s
Test "tutorial/113_accRecNoEta"
Expected: ✋ reject · Size: 13.0 KB · Lines: 244 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Acc.rec does not have structure eta.
Test result: ✋ rejected · exit code 1 · wall time: 13 ms · instructions: 16.1 M · max rss memory: 6.5 MB
stdout:
Checking 11 declarations…
stderr:
in accRecNoEta:
fun α r a h p ↦ Eq.refl.{1} Bool p
has type
(α : Type) → (r : α → ∀ (a.«_@»._internal._hyg.0 : α), Prop) → (a : α) → Acc.{1} α r a → (p : Bool) → Eq.{1} Bool p p
but is expected to have type
{α : Type} → (r : α → ∀ (a.«_@»._internal._hyg.0 : α), Prop) → (a : α) → (h : Acc.{1} α r a) → (p : Bool) → Eq.{1} Bool (Acc.rec.{1, 1} α r (fun x.«_@».Tutorial.4017164079._hygCtx._hyg.22 x.«_@».Tutorial.4017164079._hygCtx._hyg.24 ↦ Bool) (fun x.«_@».Tutorial.4017164079._hygCtx._hyg.31 x.«_@».Tutorial.4017164079._hygCtx._hyg.33 x.«_@».Tutorial.4017164079._hygCtx._hyg.35 ↦ p) a h) p
parsed in 0.001986s, checked in 0.000451s
Test "tutorial/114_quotMkType"
Expected: 👍 accept · Size: 6.3 KB · Lines: 123 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of Quot.mk.
Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 13.9 M · max rss memory: 6.0 MB
stdout:
Checking 8 declarations… All declarations are type-correct.
stderr:
parsed in 0.001356s, checked in 0.000127s
Test "tutorial/115_quotIndType"
Expected: 👍 accept · Size: 6.3 KB · Lines: 124 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of Quot.ind.
Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 14.1 M · max rss memory: 6.1 MB
stdout:
Checking 8 declarations… All declarations are type-correct.
stderr:
parsed in 0.001232s, checked in 0.000240s
Test "tutorial/116_quotLiftType"
Expected: 👍 accept · Size: 6.3 KB · Lines: 124 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of Quot.lift.
Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 14.1 M · max rss memory: 6.1 MB
stdout:
Checking 8 declarations… All declarations are type-correct.
stderr:
parsed in 0.001227s, checked in 0.000197s
Test "tutorial/117_quotSoundType"
Expected: 👍 accept · Size: 7.2 KB · Lines: 141 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of Quot.sound.
Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 14.2 M · max rss memory: 6.1 MB
stdout:
Checking 9 declarations… All declarations are type-correct.
stderr:
parsed in 0.001475s, checked in 0.000174s
Test "tutorial/118_quotLiftReduction"
Expected: 👍 accept · Size: 7.8 KB · Lines: 153 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Reduction behavior of Quot.lift on Quot.mk.
Test result: ✋ rejected · exit code 1 · wall time: 13 ms · instructions: 15.3 M · max rss memory: 6.4 MB
stdout:
Checking 8 declarations…
stderr:
in quotLiftReduction:
fun {α r β} f h a ↦ Eq.refl.{v} β (Quot.lift.{u, v} α r β f h (Quot.mk.{u} α r a))
has type
{α : Sort u} → {r : α → ∀ (a.«_@»._internal._hyg.0 : α), Prop} → {β : Sort v} → (f : α → β) → (h : (a : α) → (b : α) → r a b → Eq.{v} β (f a) (f b)) → (a : α) → Eq.{v} β (Quot.lift.{u, v} α r β f h (Quot.mk.{u} α r a)) (Quot.lift.{u, v} α r β f h (Quot.mk.{u} α r a))
but is expected to have type
{α : Sort u} → {r : α → ∀ (a.«_@»._internal._hyg.0 : α), Prop} → {β : Sort v} → (f : α → β) → (h : (a : α) → (b : α) → r a b → Eq.{v} β (f a) (f b)) → (a : α) → Eq.{v} β (Quot.lift.{u, v} α r β f h (Quot.mk.{u} α r a)) (f a)
parsed in 0.001260s, checked in 0.000748s
Test "tutorial/119_quotIndReduction"
Expected: 👍 accept · Size: 7.6 KB · Lines: 151 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Reduction behavior of Quot.ind on Quot.mk.
Test result: ✋ rejected · exit code 1 · wall time: 13 ms · instructions: 15.1 M · max rss memory: 6.4 MB
stdout:
Checking 8 declarations…
stderr:
in quotIndReduction:
fun {α} r {β} mk a ↦ Eq.refl.{0} (β (Quot.mk.{u} α r a)) (Quot.ind.{u} α r β mk (Quot.mk.{u} α r a))
has type
{α : Sort u} → (r : α → ∀ (a.«_@»._internal._hyg.0 : α), Prop) → {β : ∀ (a : Quot.{u} α r), Prop} → (mk : (a : α) → β (Quot.mk.{u} α r a)) → (a : α) → Eq.{0} (β (Quot.mk.{u} α r a)) (Quot.ind.{u} α r β mk (Quot.mk.{u} α r a)) (Quot.ind.{u} α r β mk (Quot.mk.{u} α r a))
but is expected to have type
{α : Sort u} → (r : α → ∀ (a.«_@»._internal._hyg.0 : α), Prop) → {β : ∀ (a : Quot.{u} α r), Prop} → (mk : (a : α) → β (Quot.mk.{u} α r a)) → (a : α) → Eq.{0} (β (Quot.mk.{u} α r a)) (Quot.ind.{u} α r β mk (Quot.mk.{u} α r a)) (mk a)
parsed in 0.001434s, checked in 0.000662s
Test "tutorial/120_dup_defs"
Expected: ✋ reject · Size: 479 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Two definitions with the same name
Test result: ✋ rejected · exit code 1 · wall time: 128 ms · instructions: 12.7 M · max rss memory: 5.8 MB
stderr:
RPython traceback: File "implement.c", line 25, in main File "rpylean__rcli.c", line 121, in CLI_main File "rpylean_cli.c", line 285, in check File "rpylean_cli.c", line 2685, in environment_from File "rpylean_environment.c", line 4754, in having Fatal RPython error: AlreadyDeclared
Test "tutorial/121_dup_ind_def"
Expected: ✋ reject · Size: 1.7 KB · Lines: 27 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A definition and a constructor with the same name
Test result: ✋ rejected · exit code 1 · wall time: 121 ms · instructions: 12.7 M · max rss memory: 5.8 MB
stderr:
RPython traceback: File "rpylean_cli.c", line 285, in check File "rpylean_cli.c", line 2672, in environment_from File "rpylean_environment.c", line 1309, in EnvironmentBuilder_consume File "rpylean_parser.c", line 18205, in NameStr_compile Fatal RPython error: AssertionError
Test "tutorial/122_dup_ctor_def"
Expected: ✋ reject · Size: 1.7 KB · Lines: 27 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A definition and a constructor with the same name
Test result: ✋ rejected · exit code 1 · wall time: 112 ms · instructions: 12.7 M · max rss memory: 5.8 MB
stderr:
RPython traceback: File "rpylean_cli.c", line 285, in check File "rpylean_cli.c", line 2672, in environment_from File "rpylean_environment.c", line 1309, in EnvironmentBuilder_consume File "rpylean_parser.c", line 18205, in NameStr_compile Fatal RPython error: AssertionError
Test "tutorial/123_dup_rec_def"
Expected: ✋ reject · Size: 1.7 KB · Lines: 27 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A definition and a recursor with the same name
Test result: ✋ rejected · exit code 1 · wall time: 103 ms · instructions: 12.7 M · max rss memory: 5.8 MB
stderr:
RPython traceback: File "rpylean_cli.c", line 285, in check File "rpylean_cli.c", line 2672, in environment_from File "rpylean_environment.c", line 1309, in EnvironmentBuilder_consume File "rpylean_parser.c", line 18205, in NameStr_compile Fatal RPython error: AssertionError
Test "tutorial/124_dup_rec_def2"
Expected: ✋ reject · Size: 1.7 KB · Lines: 28 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A definition with the name of a recursor, and the recursor named differently. This would pass simple checks for duplicate definitions in the parser, but should still be rejected by the checker.
Test result: ✋ rejected · exit code 1 · wall time: 104 ms · instructions: 12.7 M · max rss memory: 5.8 MB
stderr:
RPython traceback: File "rpylean_cli.c", line 285, in check File "rpylean_cli.c", line 2672, in environment_from File "rpylean_environment.c", line 1309, in EnvironmentBuilder_consume File "rpylean_parser.c", line 18205, in NameStr_compile Fatal RPython error: AssertionError
Test "tutorial/125_dup_ctor_rec"
Expected: ✋ reject · Size: 1.5 KB · Lines: 24 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A constructor and a recursor with the same name
Test result: ✋ rejected · exit code 1 · wall time: 103 ms · instructions: 12.7 M · max rss memory: 5.8 MB
stderr:
RPython traceback: File "rpylean_cli.c", line 285, in check File "rpylean_cli.c", line 2672, in environment_from File "rpylean_environment.c", line 1309, in EnvironmentBuilder_consume File "rpylean_parser.c", line 18205, in NameStr_compile Fatal RPython error: AssertionError
Test "tutorial/126_DupConCon"
Expected: ✋ reject · Size: 2.2 KB · Lines: 35 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
An inductive with two constructors with the same name
Test result: ✋ rejected · exit code 1 · wall time: 108 ms · instructions: 12.7 M · max rss memory: 5.8 MB
stderr:
RPython traceback: File "rpylean_cli.c", line 285, in check File "rpylean_cli.c", line 2672, in environment_from File "rpylean_environment.c", line 1309, in EnvironmentBuilder_consume File "rpylean_parser.c", line 18205, in NameStr_compile Fatal RPython error: AssertionError